We study from the proof complexity perspective the (informal) proof search problem (cf. [17, Sections 1.5 and 21.5]):

• • Is there an optimal way to search for propositional proofs?

We note that, as a consequence of Levin’s universal search, for any fixed proof system there exists a time-optimal proof search algorithm. Using classical proof complexity results about reflection principles we prove that a time-optimal proof search algorithm exists without restricting proof systems iff a p-optimal proof system exists.

To characterize precisely the time proof search algorithms need for individual formulas we introduce a new proof complexity measure based on algorithmic information concepts. In particular, to a proof system P we attach information-efficiency function $i_P(\tau )$ assigning to a tautology a natural number, and we show that:

• • $i_P(\tau )$ characterizes time any P-proof search algorithm has to use on $\tau $ ,

• • for a fixed P there is such an information-optimal algorithm (informally: it finds proofs of minimal information content),

• • a proof system is information-efficiency optimal (its information-efficiency function is minimal up to a multiplicative constant) iff it is p-optimal,

• • for non-automatizable systems P there are formulas $\tau $ with short proofs but having large information measure $i_P(\tau )$ .

We isolate and motivate the problem to establish unconditional super-logarithmic lower bounds for $i_P(\tau )$ where no super-polynomial size lower bounds are known. We also point out connections of the new measure with some topics in proof complexity other than proof search.

We present a forcing to obtain a localized version of Local Club Condensation, a generalized Condensation principle introduced by Sy Friedman and the first author in [3] and [5]. This forcing will have properties nicer than the forcings to obtain this localized version that could be derived from the forcings presented in either [3] or [5]. We also strongly simplify the related proofs provided in [3] and [5]. Moreover our forcing will be capable of introducing this localized principle at κ while simultaneously performing collapses to make κ become the successor of any given smaller regular cardinal. This will be particularly useful when κ has large cardinal properties in the ground model. We will apply this to measure how much L-likeness is implied by Local Club Condensation and related principles. We show that Local Club Condensation at κ+ is consistent with ¬☐κ whenever κ is regular and uncountable, generalizing and improving a result of the third author in [14], and that if κ ≥ ω2 is regular, CC(κ+) - Chang’s Conjecture at κ+ - is consistent with Local Club Condensation at κ+, both under suitable large cardinal consistency assumptions.

Analysability of finite U-rank types are explored both in general and in the theory ${\rm{DC}}{{\rm{F}}_0}$. The well-known fact that the equation $\delta \left( {{\rm{log}}\,\delta x} \right) = 0$ is analysable in but not almost internal to the constants is generalized to show that $\underbrace {{\rm{log}}\,\delta \cdots {\rm{log}}\,\delta }_nx = 0$ is not analysable in the constants in $\left( {n - 1} \right)$-steps. The notion of a canonical analysis is introduced–-namely an analysis that is of minimal length and interalgebraic with every other analysis of that length. Not every analysable type admits a canonical analysis. Using properties of reductions and coreductions in theories with the canonical base property, it is constructed, for any sequence of positive integers $\left( {{n_1}, \ldots ,{n_\ell }} \right)$, a type in ${\rm{DC}}{{\rm{F}}_0}$ that admits a canonical analysis with the property that the ith step has U-rank ${n_i}$.

In the framework of Bishop’s constructive mathematics we introduce co-convexity as a property of subsets B of ${\left\{ {0,1} \right\}^{\rm{*}}}$, the set of finite binary sequences, and prove that co-convex bars are uniform. Moreover, we establish a canonical correspondence between detachable subsets B of ${\left\{ {0,1} \right\}^{\rm{*}}}$ and uniformly continuous functions f defined on the unit interval such that B is a bar if and only if the corresponding function f is positive-valued, B is a uniform bar if and only if f has positive infimum, and B is co-convex if and only if f satisfies a weak convexity condition.

In a previous article, the author introduced the idea of intrinsic density—a restriction of asymptotic density to sets whose density is invariant under computable permutation. We prove that sets with well-defined intrinsic density (and particularly intrinsic density 0) exist only in Turing degrees that are either high (${\bf{a}}\prime { \ge _{\rm{T}}}\emptyset \prime \prime$) or compute a diagonally noncomputable function. By contrast, a classic construction of an immune set in every noncomputable degree actually yields a set with intrinsic lower density 0 in every noncomputable degree.

We also show that the former result holds in the sense of reverse mathematics, in that (over RCA0) the existence of a dominating or diagonally noncomputable function is equivalent to the existence of a set with intrinsic density 0.

It is known that every non-universal self-full degree in the structure of the degrees of computably enumerable equivalence relations (ceers) under computable reducibility has exactly one strong minimal cover. This leaves little room for embedding wide partial orders as initial segments using self-full degrees. We show that considerably more can be done by staying entirely inside the collection of non-self-full degrees. We show that the poset can be embedded as an initial segment of the degrees of ceers with infinitely many classes. A further refinement of the proof shows that one can also embed the free distributive lattice generated by the lower semilattice as an initial segment of the degrees of ceers with infinitely many classes.

We consider the model theoretic notion of convex orderability, which fits strictly between the notions of VC-minimality and dp-minimality. In some classes of algebraic theories, however, we show that convex orderability and VC-minimality are equivalent, and use this to give a complete classification of VC-minimal theories of ordered groups and abelian groups. Consequences for fields are also considered, including a necessary condition for a theory of valued fields to be quasi-VC-minimal. For example, the p-adics are not quasi-VC-minimal.

Several results in the theory of recursion in higher types indicate that the effect of a higher type functional on the lower types does not reflect the high type, i.e. the same effect could be obtained by functionals of relatively low type. The two main results here are:

Plus -1 - Theorem (G. Sacks [6] for k = 1, [7] for k > 1). Let H be a normal functional of type ≥ k + 1. Then there exists a normal functional F of type k + 1 such that k-sc(F) = k-sc(H), i.e. the same subsets of tp(k − 1) are recursive in F and H.

Plus - 2 - Theorem (L. Harrington [1]). Let H be a normal functional of type ≥ k + 2. Then there exists a normal functional F of type k +2 such that k-en(H) = k-en(F), i.e. the same subsets of tp(k − 1) are semirecursive in F and H.

The results in this paper also indicate that higher types cannot have too much influence on lower types. The key is the Skolem-Löwenheim theorem. Among the results we mention:

(1) Let n < m. A ⊆ tp(n) × tp(m) be Kleene-semicomputable. Let x ∈ B ⇔ ∀y∈tp(m), ⟨x, y⟩ ∈ A. Then B is . This result may be relativized to a functional of type n + 1.

(2) Let k0 be the type-k-functional that is constant zero. Let F be a functional of type < k. Then, for i ≤ k −2, i-sc(F ,k0) = i-sc(F), i-en(F, k0) = ∀tp(i)(i-en(F)).

Let be a finite sequence of algebras of sets given on a set with more than pairwise disjoint sets not belonging to It was shown in [4] and [5] that in this case Let us consider, instead a finite sequence of algebras It turns out that if for each natural i ≤ l there exist no less than pairwise disjoint sets not belonging to then But if l ≥ 195 and if for each natural i ≤ l there exist no less than pairwise disjoint sets not belonging to then After consideration of finite sequences of algebras, it is natural to consider countable sequences of algebras. We obtained two essentially important theorems on a countable sequence of almost σ-algebras (the concept of almost σ-algebra was introduced in [4]).

It was J. E. Baumgartner who in [1] proved that when a weakly compact cardinal is Lévy-collapsed to ω2 the new ω2 inherits some of the large cardinal properties; e.g. if S is a stationary set of ω-limits in ω2 then for some α < ω2, S ∩ α is stationary in α. Later S. Shelah extended this to the following theorem: if a supercompact cardinal κ is Lévy-collapsed to ω2, then in the resulting model the following holds: if S ⊆ λ is a stationary set of ω-limits and cf(λ) ≥ ω2 then there is an α. < λ such that S ∩ α is stationary in α, i.e. stationary reflection holds for countable cofinality (see [1] and [3]). These theorems are important prototypes of small cardinal compactness theorems; many applications and generalizations can be found in the literature. One might think that these results are true for sets with an uncountable cofinality μ as well, i.e. when an appropriate large cardinal is collapsed to μ++. Though this is true for Baumgartner's theorem, there remains a problem with Shelah's result. The point is that the lemma stating that a stationary set of ω-limits remains stationary after forcing with an ω2-closed partial order may be false in the case of μ-limits in a cardinal of the form λ+ with cf(λ) < μ, as was shown in [8] by Shelah. The problem has recently been solved by Baumgartner, who observed that if a universal box-sequence on the class of those ordinals with cofinality ≤ μ exists, the lemma still holds, and a universal box-sequence of the above type can be added without destroying supercompact cardinals beyond μ.

We answer some questions from [4] by giving suitable examples of small Polish structures. First, we present a class of small Polish group structures without generic elements. Next, we construct a first example of a small non-zero-dimensional Polish G-group.

Where AR is the set of arithmetic Turing degrees, 0(ω) is the least member of {a(2) ∣ a is an upper bound on AR}. This situation is quite different if we examine HYP, the set of hyperarithmetic degrees. We shall prove (Corollary 1) that there is an a, an upper bound on HYP, whose hyperjump is the degree of Kleene's . This paper generalizes this example, using an iteration of the jump operation into the transfinite which is based on results of Jensen and is detailed in [3] and [4]. In § 1 we review the basic definitions from [3] which are needed to state the general results.