The complexity of the modal predicate logic of “true in every transitive model of ZF”

1997 ◽  
Vol 62 (4) ◽  
pp. 1371-1378
Author(s):  
Vann McGee
Keyword(s):  
Lower Bound ◽  
Set Theory ◽  
Predicate Logic ◽  
Alternative Conception ◽  
Predicate Calculus ◽  
Modal Formula ◽  
Sentential Calculus ◽  
Transitive Model ◽  
Modal Predicate Logic

Robert Solovay [8] investigated the version of the modal sentential calculus one gets by taking “□ϕ” to mean “ϕ is true in every transitive model of Zermelo-Fraenkel set theory (ZF).” Defining an interpretation to be a function * taking formulas of the modal sentential calculus to sentences of the language of set theory that commutes with the Boolean connectives and sets (□ϕ)* equal to the statement that ϕ* is true in every transitive model of ZF, and stipulating that a modal formula ϕ is valid if and only if, for every interpretation *, ϕ* is true in every transitive model of ZF, Solovay obtained a complete and decidable set of axioms.In this paper, we stifle the hope that we might continue Solovay's program by getting an analogous set of axioms for the modal predicate calculus. The set of valid formulas of the modal predicate calculus is not axiomatizable; indeed, it is complete .We also look at a variant notion of validity according to which a formula ϕ counts as valid if and only if, for every interpretation *, ϕ* is true. For this alternative conception of validity, we shall obtain a lower bound of complexity: every set which is in the set of sentences of the language of set theory true in the constructible universe will be 1-reducible to the set of valid modal formulas.

On the degrees of unsolvability of modal predicate logics of provability

1994 ◽  
Vol 59 (1) ◽  
pp. 253-261
Author(s):  
Vann McGee
Keyword(s):  
Predicate Logic ◽  
General Theorem ◽  
Modal Formula ◽  
Sentential Logic ◽  
Starting Point ◽  
Special Cases ◽  
Modal Predicate Logics ◽  
Arithmetical Formula ◽  
Modal Predicate Logic ◽  
Striking Contrast

The modal predicate logic of provability identifies the “□” of modal logic with the “Bew” of proof theory, so that, where “Bew” is a formula representing, in the usual way, provability in a consistent, recursively axiomatized theory Γ extending Peano arithmetic (PA), an interpretation of a language for the modal predicate calculus is a map * which associates with each modal formula an arithmetical formula with the same free variables which commutes with the Boolean connectives and the quantifiers and which sets (□ϕ)* equal to Bew(⌈ϕ*⌉). Where Δ is an extension of PA (all the theories we discuss will be extensions of PA), MPL(Δ) will be the set of modal formulas ϕ such that, for every interpretation *, ϕ* is a theorem of Δ. Most of what is currently known about the modal predicate logic of provability consists in demonstrations that MPL(Δ) must be computationally highly complex. Thus Vardanyan [11] shows that, provided that Δ is 1-consistent and recursively axiomatizable, MPL(Δ) will be complete , and Boolos and McGee [5] show that MPL({true arithmetical sentences}) is complete in {true arithmetical sentences}. All of these results take as their starting point Artemov's demonstration in [1] that {true arithmetical sentences} is 1-reducible to MPL({true arithmetical sentences}).The aim here is to consolidate these results by providing a general theorem which yields all the other results as special cases. These results provide a striking contrast with the situation in modal sentential logic (MSL); according to fundamental results of Solovay [8], provided Γ does not entail any falsehoods, MSL({true arithmetical sentences}) and MSL(PA) (which is the same as MSL(Γ)) are both decidable.

Constructible lattices of c-degrees

1982 ◽  
Vol 47 (4) ◽  
pp. 739-754
Author(s):  
C.P. Farrington
Keyword(s):  
Set Theory ◽  
Regular Cardinal ◽  
Boolean Algebras ◽  
Combinatorial Complexity ◽  
Generic Extension ◽  
Transitive Model ◽  
Perfect Set ◽  
Consistency Results ◽  
Combinatorial Principles ◽  
Souslin Trees

This paper is devoted to the proof of the following theorem.Theorem. Let M be a countable standard transitive model of ZF + V = L, and let ℒ Є M be a wellfounded lattice in M, with top and bottom. Let ∣ℒ∣M = λ, and suppose κ ≥ λ is a regular cardinal in M. Then there is a generic extension N of M such that(i) N and M have the same cardinals, and κN ⊂ M;(ii) the c-degrees of sets of ordinals of N form a pattern isomorphic to ℒ;(iii) if A ⊂ On and A Є N, there is B Є P(κ+)N such that L(A) = L(B).The proof proceeds by forcing with Souslin trees, and relies heavily on techniques developed by Jech. In [5] he uses these techniques to construct simple Boolean algebras in L, and in [6] he uses them to construct a model of set theory whose c-degrees have orderlype 1 + ω*.The proof also draws on ideas of Adamovicz. In [1]–[3] she obtains consistency results concerning the possible patterns of c-degrees of sets of ordinals using perfect set forcing and symmetric models. These methods have the advantage of yielding real degrees, but involve greater combinatorial complexity, in particular the use of ‘sequential representations’ of lattices.The advantage of the approach using Souslin trees is twofold: first, we can make use of ready-made combinatorial principles which hold in L, and secondly, the notion of genericity over a Souslin tree is particularly simple.

Combinator realizability of a constructive Morse set theory

1974 ◽  
Vol 39 (2) ◽  
pp. 226-234
Author(s):  
John Staples
Keyword(s):  
Set Theory ◽  
Predicate Calculus ◽  
Constructive Version

A constructive version of Morse set theory is given, based on Heyting's predicate calculus and with countable rather than full choice. An elaboration of the method of [5] is used to show that the theory is combinator-realizable in the sense defined there. The proof depends on the assumption of the syntactic consistency of the theory.The method is introduced by first treating a subtheory without countable choice of foundation.It is intended that the work can be read either classically or constructively, though whether the word constructive is correctly used as a description of either the theory or the metatheory is of course a matter of opinion.

On generic extensions without the axiom of choice

1983 ◽  
Vol 48 (1) ◽  
pp. 39-52 ◽  
Author(s):  
G. P. Monro
Keyword(s):  
Set Theory ◽  
Axiom Of Choice ◽  
Generic Extension ◽  
Transitive Model ◽  
The Axiom Of Choice ◽  
Generic Extensions

AbstractLet ZF denote Zermelo-Fraenkel set theory (without the axiom of choice), and let M be a countable transitive model of ZF. The method of forcing extends M to another model M[G] of ZF (a “generic extension”). If the axiom of choice holds in M it also holds in M[G], that is, the axiom of choice is preserved by generic extensions. We show that this is not true for many weak forms of the axiom of choice, and we derive an application to Boolean toposes.

On the formalisation of indirect discourse

1958 ◽  
Vol 23 (4) ◽  
pp. 417-419 ◽  
Author(s):  
R. L. Goodstein
Keyword(s):  
Predicate Logic ◽  
Logical Truth ◽  
Predicate Calculus ◽  
Inference Rules ◽  
First Order ◽  
Indirect Discourse ◽  
Image Position ◽  
Order Predicate Calculus

Mr. L. J. Cohen's interesting example of a logical truth of indirect discourse appears to be capable of a simple formalisation and proof in a variant of first order predicate calculus. His example has the form:If A says that anything which B says is false, and B says that something which A says is true, then something which A says is false and something which B says is true.Let ‘A says x’ be formalised by ‘A(x)’ and let assertions of truth and falsehood be formalised as in the following table.We treat both variables x and predicates A (x) as sentences and add to the familiar axioms and inference rules of predicate logic a rule permitting the inference of A(p) from (x)A(x), where p is a closed sentence.We have to prove that from

Sign in / Sign up

Export Citation Format

Share Document