Chain Logic

  • Chain Logic is denoted as
  • There is no difference in the syntax between and , instead there is a semantic difference. Take any model of power at least , will be seen as a filtration of subsets of its domain A (), that is with . The difference is in the interpretation of infinitary quantifiers: there exists and with i.e., quantification is bounded by a level of the filtration E.g., Impacts defined the well-order while in you cannot.

Infinitely Deep Logic

  • Formulas of the language are regarded as trees of symbols. i.e., is a triple where is a tree-structure and {} {} where is the set of atomic formulas of with vocabulary and is a set of ‘enough’ variables.
  • The function must satisfy the following:
    • will form a tree of symbols
    • if is or then has immediate successors
    • when {}{}, then has one immediate successor
    • for then has no successors

Shelah’s Infinitary Logic

  • Shelah’s Infinitary Logic is denoted as
  • has no syntax, instead it is defined via a variation of Ehrenfeucht–Fraïssé games (a technique to determine if two structures are elementary equivalent, via a back-and-forth game)
  • Consider two models and , and then define . We want to prove that is an equivalence relation, so we define another relation which is the transitive closure of . Each is a union of -equivalence relations. Formulas are equivalence classes consisting of models.
  • Results:
  • Approximation of syntax:

Sort Logic

  • A many-sorted extension of second-order logic which can quantify and reason over its own structures (has the ability to “look outside” the model). e.g., It can make references to objects outside of the domain Consider a Turing machine, which is defined as a finite set of quadruples, to halt require reference to a tape potentially larger than the Turing machine itself Allows it to be stronger than order logic for an arbitrary ordinal (and set theory) i.e., Sort Logic allows for -iterations of the powerset over arbitrary sets, for is an arbitrary ordinal. This is because the -quantifier introduces new sorts of objects which may be arbitrary (not necessarily the powerset of the previous sort like how types are created Type Theory) . -order logic only allows -iterations of the powerset of a given (initial) domain. Sort Logic describes sets that are not in the transitive closure of a model (i.e., the least transitive set containing as a subset), TC().

  • Every model class definable in set theory is the class of models of a sentence of sort logic. i.e., For any model class (of a -sentence), there exists a sentence such that

  • Sort Logic retains the structuralist approach to mathematics. Recall: The structuralist perspective of mathematics asserts that mathematical theories describe structures of mathematics, structures are defined by their properties (i.e., s(n) = n+1 for the natural numbers ). Different mathematical systems can interpret the same structure in different ways (i.e., the structure exists independently of the mathematical system, this is in contrast to views where structures are seen as relative or dependent on mathematical system). This is related to mathematical Platonism (a mathematical system - i.e., ZFC - describes the universe of sets). See Philosophy of Sets & Proper-Classes

  • Considered the “strongest” model theoretic logic ( any ‘extension’ is effectively redundant?)

The classes (for ) of the Levy hierarchy of formulas can be considered as sub-logics (or more appropriately as sets of sentences of sort logic) of sort logic as it characterizes any model class. The Hanf number and Löwenheim number of the logic of is and respectively. Thus, it can be observed that the canonical hierarchy of climbs up the large cardinal hierarchy (in fact, up to Vopenka’s Principle) with reference to Hanf and Löwenheim numbers

The decision problem (see Turing Machines & Computability Theory) of the logic is the complete set of natural numbers.

Note: Sort logic is a finitary logic (i.e., only allows finitely-long formulae) and thus has an occurrence number of . is set-sized (i.e., for is some cardinal) due to having only two forms of quantification, first-order quantification and sort quantification. Thus, sort logic also has a Hanf and Löwenheim number (The Hanf Number, The Löwenheim Number).

  • Sort logic is the ‘strongest’ logic relative to set theory (ZFC) as it can characterize model classes for any formula of the levy hierarchy. Note: that characterizing (the size) a model characterizing a model class), i.e., capture and being able to differentiate between sizes of infinity. Can consider an extension of sort logic which does characterize the size of it’s models (sort logic being the ‘strongest logic’ seems to refer to its ability to characterize model classes specifically). Recall: Expressive power deals with elementary-classes and defining model classes…,etc. (for other notions of expressive power, see Logics, Structures & Models) .Thus, the notion of ‘expressive strength’ is tied to characterizing model classes. We are using a different ‘measuring stick’ when measuring expressive power by the characterizability of (individual) models through Hanf numbers and Löwenheim numbers. So this ‘extension’ will not increase expressive power.

Syntax: Sort Logic has the additional quantifiers and , with '' meaning that there is a predicate of new sorts of elements of such that (whatever) i.e., posits that there exists a new sort of objects not apart of the current model and a relation on such objects such that holds. express the existence of a structure outside of the model, internally w/in the model you can formalize extensions of the universe. Note: logic with multiple sorts allow for quantification over objects across multiple sorts

Note: Even though sort logic can ‘see’ outside of the model, it still follows Incompleteness theorem and Tarski’s undefinability theorem (so it cannot define its own truth predicate and semantics).

  • The Completeness Theorem holds for sort logic, meaning all statements true in a model of sort logic is provable.

What differentiates sort logic from set theory? Sort logic and set theory are similar but sort logic is a logic, and sort logic treats mathematical structures up to isomorphism only (structuralist view)

Intuitionistic/Constructive Logic

In intuitionistic logic, a sentence is true iff it is provable (thus collapsing the wall between syntax and semantics in a sense). Intuitionistic logics rejects the law of excluded middle and double negation elimination but are still bivalent (i.e., Truth states ) unlike paracomplete logics. This implies that both and can both have not proofs. E.g., since double negation elimination is rejected, not

Philosophically, it can be seen that intuitionistic logic conflates syntax and semantics in that semantics is directly informed by syntax (whether or not a statement has proof). Thus, rejecting Tarski’s theory of truth (the T-schema).

For an existential sentence, you must know what exact elements satisfies the sentence in order to prove. Intuitionists do not believe in a inference from negative information to positive information, (i.e., ).

In intuitionistic logic, material implication, is not necessarily equivalent to (unless it can be shown to be).

Pierce’s law: , does not hold in intuitionistic logic

Intuitionistic logic can be modelled using modal logic

BHK Interpretation

The connectives can be interpreted in the following way: - if there is a proof of and a proof of - if there is a proof of or a proof of - is a proof construction that transforms any proof of into a proof of - is the same as

If something doesn’t have a proof nor a disproof then the sentence is independent, this is interpreted in intuitionistic logic as it being neither true nor false (w/out the actual third truth state).

Glivenko’s Translation: For is a propositional formula, then is a tautology in classical logic (i.e., ) if and only if is a tautology in intuitionistic logic (i.e., ).


Bi-intuitionistic logic is an extension of intuitionistic logic which adds co-implication or exclusion connective, denoted or \ which is dual to implication. This connective expresses that there cannot be a proof (or ‘construction’) from a sentence to another, effectively telling us what we cannot prove.

E.g., in intuitionistic logic expresses “from any construction of we can obtain a construction of ”, while \ expresses “a construction of from which a construction of is not possible.”

(This is the same as informally in propositional logic, however in this case there is a dedicated symbol expressing this in the syntax so it is formal).

Cardinality Quantifier Logics

An additional quantifier added to the set of logical symbols. can mean “there are countably-many”, or “there are uncountably-many .” Cardinality quantifiers can be further specified so you are ranging over an exact number of things, i.e., the quantifier means “there are -many”

Model Theoretic Logics

Quantum Logic

Developed to model quantum mechanics. In quantum logic the distributivity law fails (i.e., ). E.g., consider the following sentences

  • “the electron has x-spin up”
  • “the electron has y-spin up”
  • “the electron has y-spin down” Whenever spin is measured in the y-axis, then it is either up or down: i.e., and so trivially, .

Suppose is true, then , while

Quantum logic is modelled via lattices…

Failure of the deduction theorem

References

Sort Logic.pdf Model Theoretic Logics