Intermediate logic

Last updated

In mathematical logic, a superintuitionistic logic is a propositional logic extending intuitionistic logic. Classical logic is the strongest consistent superintuitionistic logic; thus, consistent superintuitionistic logics are called intermediate logics (the logics are intermediate between intuitionistic logic and classical logic). [1]

Contents

Definition

A superintuitionistic logic is a set L of propositional formulas in a countable set of variables pi satisfying the following properties:

1. all axioms of intuitionistic logic belong to L;
2. if F and G are formulas such that F and FG both belong to L, then G also belongs to L (closure under modus ponens);
3. if F(p1, p2, ..., pn) is a formula of L, and G1, G2, ..., Gn are any formulas, then F(G1, G2, ..., Gn) belongs to L (closure under substitution).

Such a logic is intermediate if furthermore

4. L is not the set of all formulas.

Properties and examples

There exists a continuum of different intermediate logics and just as many such logics exhibit the disjunction property (DP). Superintuitionistic or intermediate logics form a complete lattice with intuitionistic logic as the bottom and the inconsistent logic (in the case of superintuitionistic logics) or classical logic (in the case of intermediate logics) as the top. Classical logic is the only coatom in the lattice of superintuitionistic logics; the lattice of intermediate logics also has a unique coatom, namely SmL[ citation needed ].

The tools for studying intermediate logics are similar to those used for intuitionistic logic, such as Kripke semantics. For example, Gödel–Dummett logic has a simple semantic characterization in terms of total orders. Specific intermediate logics may be given by semantical description.

Others are often given by adding one or more axioms to

Examples include:

= IPC + ¬¬pp (Double-negation elimination, DNE)
= IPC + (¬pp) → p (Consequentia mirabilis)
= IPC + p ∨ ¬p (Principle of excluded middle, PEM)

Generalized variants of the above (but actually equivalent principles over intuitionistic logic) are, respectively,

= IPC + (¬p → ¬q) → (qp) (inverse contraposition principle)
= IPC + ((pq) → p) → p (Pierce's principle PP, compare to Consequentia mirabilis)
= IPC + (qp) → ((¬qp) → p) (another schema generalizing Consequentia mirabilis)
= IPC + p ∨ (pq) (following from PEM via principle of explosion)
= IPC + (¬qp) → (((pq) → p) → p) (a conditional PP)
= IPC + (pq) ∨ (qp) (Dirk Gently’s principle, DGP, or linearity)
= IPC + (p → (qr)) → ((pq) ∨ (pr)) (a form of independence of premise IP)
= IPC + ((pq) → r) → ((pr) ∨ (qr)) (Generalized 4th De Morgan's law)
= IPC + p ∨ (p → (q ∨ ¬q))
= IPC + ¬¬p ∨ ¬p (weak PEM, a.k.a. WPEM)
= IPC + (pq) ∨ (¬p → ¬q) (a weak DGP)
= IPC + (p → (q ∨ ¬r)) → ((pq) ∨ (p → ¬r)) (a variant, with negation, of a form of IP)
= IPC + ¬(pq) → (¬q ∨ ¬p) (4th De Morgan's law)
= IPC + ((¬¬pp) → (p ∨ ¬p)) → (¬¬p ∨ ¬p) (a conditional WPEM)
= IPC + (¬p → (qr)) → ((¬pq) ∨ (¬pr)) (the other variant, with negation, of a form of IP)

This list is, for the most part, not any sort of ordering. For example, LC is known not to prove all theorems of SmL, but it does not directly compare in strength to BD2. Likewise, e.g., KP does not compare to SL. The list of equalities for each logic is by no means exhaustive either. For example, as with WPEM and De Morgan's law, several forms of DGP using conjunction may be expressed.

Even (¬¬p ∨ ¬p) ∨ (¬¬pp), a further weakening of WPEM, is not a theorem of IPC.

It may also be worth noting that, taking all of intuitionistic logic for granted, the equalities notably rely on explosion. For example, over mere minimal logic, as principle PEM is already equivalent to Consequentia mirabilis, but there does not imply the stronger DNE, nor PP, and is not comparable to DGP.

Going on:

IPC + pn ∨ (pn → (pn−1 ∨ (pn−1 → ... → (p2 ∨ (p2 → (p1 ∨ ¬p1)))...)))
LC + BDn−1
= LC + BCn−1

Furthermore:

The propositional logics SL and KP do have the disjunction property DP. Kleene realizability logic and the strong Medvedev's logic do have it as well. There is no unique maximal logic with DP on the lattice. Note that if a consistent theory validates WPEM but still has independent statements when assuming PEM, then it cannot have DP.

Semantics

Given a Heyting algebra H, the set of propositional formulas that are valid in H is an intermediate logic. Conversely, given an intermediate logic it is possible to construct its Lindenbaum–Tarski algebra, which is then a Heyting algebra.

An intuitionistic Kripke frame F is a partially ordered set, and a Kripke model M is a Kripke frame with valuation such that is an upper subset of F. The set of propositional formulas that are valid in F is an intermediate logic. Given an intermediate logic L it is possible to construct a Kripke model M such that the logic of M is L (this construction is called the canonical model). A Kripke frame with this property may not exist, but a general frame always does.

Relation to modal logics

Let A be a propositional formula. The Gödel–Tarski translation of A is defined recursively as follows:

If M is a modal logic extending S4 then ρM = {A | T(A) ∈ M} is a superintuitionistic logic, and M is called a modal companion of ρM. In particular:

For every intermediate logic L there are many modal logics M such that L = ρM.

See also

Notes

  1. "Intermediate logic", Encyclopedia of Mathematics , EMS Press, 2001 [1994].
  2. Terwijn 2006.
  3. Medvedev 1962.
  4. Medvedev 1963.
  5. Medvedev 1966.

Related Research Articles

In logic, the law of excluded middle or the principle of excluded middle states that for every proposition, either this proposition or its negation is true. It is one of the three laws of thought, along with the law of noncontradiction, and the law of identity; however, no system of logic is built on just these laws, and none of these laws provides inference rules, such as modus ponens or De Morgan's laws. The law is also known as the law / principleof the excluded third, in Latin principium tertii exclusi. Another Latin designation for this law is tertium non datur or "no third [possibility] is given". In classical logic, the law is a tautology.

<span class="mw-page-title-main">Logical connective</span> Symbol connecting sentential formulas in logic

In logic, a logical connective is a logical constant. Connectives can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary connective can be used to join the two atomic formulas and , rendering the complex formula .

The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, biconditional, and negation. Some sources include other connectives, as in the table below.

<span class="mw-page-title-main">Saul Kripke</span> American philosopher and logician (1940–2022)

Saul Aaron Kripke was an American analytic philosopher and logician. He was Distinguished Professor of Philosophy at the Graduate Center of the City University of New York and emeritus professor at Princeton University. Since the 1960s, he has been a central figure in a number of fields related to mathematical and modal logic, philosophy of language and mathematics, metaphysics, epistemology, and recursion theory.

<span class="mw-page-title-main">Negation</span> Logical operation

In logic, negation, also called the logical not or logical complement, is an operation that takes a proposition to another proposition "not ", standing for " is not true", written , or . It is interpreted intuitively as being true when is false, and false when is true. Negation is thus a unary logical connective. It may be applied as an operation on notions, propositions, truth values, or semantic values more generally. In classical logic, negation is normally identified with the truth function that takes truth to falsity. In intuitionistic logic, according to the Brouwer–Heyting–Kolmogorov interpretation, the negation of a proposition is the proposition whose proofs are the refutations of .

Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.

In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics.

In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the natural style of deduction used by mathematicians than to David Hilbert's earlier style of formal logic, in which every line was an unconditional tautology. More subtle distinctions may exist; for example, propositions may implicitly depend upon non-logical axioms. In that case, sequents signify conditional theorems in a first-order language rather than conditional tautologies.

In mathematics, a Heyting algebra (also known as pseudo-Boolean algebra) is a bounded lattice (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation ab of implication such that (ca) ≤ b is equivalent to c ≤ (ab). From a logical standpoint, AB is by this definition the weakest proposition for which modus ponens, the inference rule AB, AB, is sound. Like Boolean algebras, Heyting algebras form a variety axiomatizable with finitely many equations. Heyting algebras were introduced by Arend Heyting (1930) to formalize intuitionistic logic.

Paraconsistent logic is an attempt at a logical system to deal with contradictions in a discriminating way. Alternatively, paraconsistent logic is the subfield of logic that is concerned with studying and developing "inconsistency-tolerant" systems of logic, which reject the principle of explosion.

Kripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Joyal. It was first conceived for modal logics, and later adapted to intuitionistic logic and other non-classical systems. The development of Kripke semantics was a breakthrough in the theory of non-classical logics, because the model theory of such logics was almost non-existent before Kripke.

In logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is already derivable without that rule, so, in a sense, it is redundant. The concept of an admissible rule was introduced by Paul Lorenzen (1955).

In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer and Arend Heyting, and independently by Andrey Kolmogorov. It is also sometimes called the realizability interpretation, because of the connection with the realizability theory of Stephen Kleene. It is the standard explanation of intuitionistic logic.

In mathematical logic, Craig's interpolation theorem is a result about the relationship between different logical theories. Roughly stated, the theorem says that if a formula φ implies a formula ψ, and the two have at least one atomic variable symbol in common, then there is a formula ρ, called an interpolant, such that every non-logical symbol in ρ occurs both in φ and ψ, φ implies ρ, and ρ implies ψ. The theorem was first proved for first-order logic by William Craig in 1957. Variants of the theorem hold for other logics, such as propositional logic. A stronger form of Craig's interpolation theorem for first-order logic was proved by Roger Lyndon in 1959; the overall result is sometimes called the Craig–Lyndon theorem.

Epistemic modal logic is a subfield of modal logic that is concerned with reasoning about knowledge. While epistemology has a long philosophical tradition dating back to Ancient Greece, epistemic logic is a much more recent development with applications in many fields, including philosophy, theoretical computer science, artificial intelligence, economics and linguistics. While philosophers since Aristotle have discussed modal logic, and Medieval philosophers such as Avicenna, Ockham, and Duns Scotus developed many of their observations, it was C. I. Lewis who created the first symbolic and systematic approach to the topic, in 1912. It continued to mature as a field, reaching its modern form in 1963 with the work of Kripke.

Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.

In logic, a modal companion of a superintuitionistic (intermediate) logic L is a normal modal logic that interprets L by a certain canonical translation, described below. Modal companions share various properties of the original intermediate logic, which enables to study intermediate logics using tools developed for modal logic.

Dynamic epistemic logic (DEL) is a logical framework dealing with knowledge and information change. Typically, DEL focuses on situations involving multiple agents and studies how their knowledge changes when events occur. These events can change factual properties of the actual world : for example a red card is painted in blue. They can also bring about changes of knowledge without changing factual properties of the world : for example a card is revealed publicly to be red. Originally, DEL focused on epistemic events. We only present in this entry some of the basic ideas of the original DEL framework; more details about DEL in general can be found in the references.

In mathematical logic, the hypersequent framework is an extension of the proof-theoretical framework of sequent calculi used in structural proof theory to provide analytic calculi for logics that are not captured in the sequent framework. A hypersequent is usually taken to be a finite multiset of ordinary sequents, written

Inquisitive semantics is a framework in logic and natural language semantics. In inquisitive semantics, the semantic content of a sentence captures both the information that the sentence conveys and the issue that it raises. The framework provides a foundation for the linguistic analysis of statements and questions. It was originally developed by Ivano Ciardelli, Jeroen Groenendijk, Salvador Mascarenhas, and Floris Roelofsen.

References