Intuitionistic logic

From Wikipedia for FEVERv2
Jump to navigation Jump to search

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. Intuitionistic logic_sentence_0

In particular, systems of intuitionistic logic do not include the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic. Intuitionistic logic_sentence_1

Formalized intuitionistic logic was originally developed by Arend Heyting to provide a formal basis for Brouwer's programme of intuitionism. Intuitionistic logic_sentence_2

From a proof-theoretic perspective, Heyting’s calculus is a restriction of classical logic in which the law of excluded middle and double negation elimination have been removed. Intuitionistic logic_sentence_3

Excluded middle and double negation elimination can still be proved for some propositions on a case by case basis, however, but do not hold universally as they do with classical logic. Intuitionistic logic_sentence_4

Several systems of semantics for intuitionistic logic have been studied. Intuitionistic logic_sentence_5

One of these semantics mirrors classical Boolean-valued semantics but uses Heyting algebras in place of Boolean algebras. Intuitionistic logic_sentence_6

Another semantics uses Kripke models. Intuitionistic logic_sentence_7

These, however, are technical means for studying Heyting’s deductive system rather than formalizations of Brouwer’s original informal semantic intuitions. Intuitionistic logic_sentence_8

Semantical systems claiming to capture such intuitions, due to offering meaningful concepts of “constructive truth” (rather than merely validity or provability), are Gödel’s dialectica interpretation, Kleene’s realizability, Yurii Medvedev’s logic of finite problems, or Japaridze’s computability logic. Intuitionistic logic_sentence_9

Yet such semantics persistently induce logics properly stronger than Heyting’s logic. Intuitionistic logic_sentence_10

Some authors have argued that this might be an indication of inadequacy of Heyting’s calculus itself, deeming the latter incomplete as a constructive logic. Intuitionistic logic_sentence_11

Mathematical constructivism Intuitionistic logic_section_0

Intuitionistic logic is a commonly-used tool in developing approaches to constructivism in mathematics. Intuitionistic logic_sentence_12

The use of constructivist logics in general has been a controversial topic among mathematicians and philosophers (see, for example, the Brouwer–Hilbert controversy). Intuitionistic logic_sentence_13

A common objection to their use is the above-cited lack of two central rules of classical logic, the law of excluded middle and double negation elimination. Intuitionistic logic_sentence_14

These are considered to be so important to the practice of mathematics that David Hilbert wrote of them: "Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists. Intuitionistic logic_sentence_15

To prohibit existence statements and the principle of excluded middle is tantamount to relinquishing the science of mathematics altogether." Intuitionistic logic_sentence_16

Despite the serious challenges presented by the inability to utilize the valuable rules of excluded middle and double negation elimination, intuitionistic logic has practical use. Intuitionistic logic_sentence_17

One reason for this is that its restrictions produce proofs that have the existence property, making it also suitable for other forms of mathematical constructivism. Intuitionistic logic_sentence_18

Informally, this means that if there is a constructive proof that an object exists, that constructive proof may be used as an algorithm for generating an example of that object, a principle known as the Curry–Howard correspondence between proofs and algorithms. Intuitionistic logic_sentence_19

One reason that this particular aspect of intuitionistic logic is so valuable is that it enables practitioners to utilize a wide range of computerized tools, known as proof assistants. Intuitionistic logic_sentence_20

These tools assist their users in the verification (and generation) of large-scale proofs, whose size usually precludes the usual human-based checking that goes into publishing and reviewing a mathematical proof. Intuitionistic logic_sentence_21

As such, the use of proof assistants (such as Agda or Coq) is enabling modern mathematicians and logicians to develop and prove extremely complex systems, beyond those that are feasible to create and check solely by hand. Intuitionistic logic_sentence_22

One example of a proof that was impossible to satisfactorily verify without formal verification is the famous proof of the four color theorem. Intuitionistic logic_sentence_23

This theorem stumped mathematicians for more than a hundred years, until a proof was developed that ruled out large classes of possible counterexamples, yet still left open enough possibilities that a computer program was needed to finish the proof. Intuitionistic logic_sentence_24

That proof was controversial for some time, but, later, it was verified using Coq. Intuitionistic logic_sentence_25

Syntax Intuitionistic logic_section_1

The syntax of formulas of intuitionistic logic is similar to propositional logic or first-order logic. Intuitionistic logic_sentence_26

However, intuitionistic connectives are not definable in terms of each other in the same way as in classical logic, hence their choice matters. Intuitionistic logic_sentence_27

In intuitionistic propositional logic (IPL) it is customary to use →, ∧, ∨, ⊥ as the basic connectives, treating ¬A as an abbreviation for (A → ⊥). Intuitionistic logic_sentence_28

In intuitionistic first-order logic both quantifiers ∃, ∀ are needed. Intuitionistic logic_sentence_29

Weaker than classical logic Intuitionistic logic_section_2

Sequent calculus Intuitionistic logic_section_3

Main article: Sequent calculus Intuitionistic logic_sentence_30

Gerhard Gentzen discovered that a simple restriction of his system LK (his sequent calculus for classical logic) results in a system that is sound and complete with respect to intuitionistic logic. Intuitionistic logic_sentence_31

He called this system LJ. Intuitionistic logic_sentence_32

In LK any number of formulas is allowed to appear on the conclusion side of a sequent; in contrast LJ allows at most one formula in this position. Intuitionistic logic_sentence_33

Other derivatives of LK are limited to intuitionistic derivations but still allow multiple conclusions in a sequent. Intuitionistic logic_sentence_34

LJ' is one example. Intuitionistic logic_sentence_35

Hilbert-style calculus Intuitionistic logic_section_4

Intuitionistic logic can be defined using the following Hilbert-style calculus. Intuitionistic logic_sentence_36

This is similar to a way of axiomatizing classical propositional logic. Intuitionistic logic_sentence_37

In propositional logic, the inference rule is modus ponens Intuitionistic logic_sentence_38

and the axioms are Intuitionistic logic_sentence_39

To make this a system of first-order predicate logic, the generalization rules Intuitionistic logic_sentence_40

are added, along with the axioms Intuitionistic logic_sentence_41

Optional connectives Intuitionistic logic_section_5

Negation Intuitionistic logic_section_6
Equivalence Intuitionistic logic_section_7

Relation to classical logic Intuitionistic logic_section_8

The system of classical logic is obtained by adding any one of the following axioms: Intuitionistic logic_sentence_42

Another relationship is given by the Gödel–Gentzen negative translation, which provides an embedding of classical first-order logic into intuitionistic logic: a first-order formula is provable in classical logic if and only if its Gödel–Gentzen translation is provable intuitionistically. Intuitionistic logic_sentence_43

Therefore, intuitionistic logic can instead be seen as a means of extending classical logic with constructive semantics. Intuitionistic logic_sentence_44

In 1932, Kurt Gödel defined a system of logics intermediate between classical and intuitionistic logic; Gödel logics are concomitantly known as intermediate logics. Intuitionistic logic_sentence_45

Non-interdefinability of operators Intuitionistic logic_section_9

In classical propositional logic, it is possible to take one of conjunction, disjunction, or implication as primitive, and define the other two in terms of it together with negation, such as in Łukasiewicz's three axioms of propositional logic. Intuitionistic logic_sentence_46

It is even possible to define all four in terms of a sole sufficient operator such as the Peirce arrow (NOR) or Sheffer stroke (NAND). Intuitionistic logic_sentence_47

Similarly, in classical first-order logic, one of the quantifiers can be defined in terms of the other and negation. Intuitionistic logic_sentence_48

These are fundamentally consequences of the law of bivalence, which makes all such connectives merely Boolean functions. Intuitionistic logic_sentence_49

The law of bivalence is not required to hold in intuitionistic logic, only the law of non-contradiction. Intuitionistic logic_sentence_50

As a result, none of the basic connectives can be dispensed with, and the above axioms are all necessary. Intuitionistic logic_sentence_51

Most of the classical identities are only theorems of intuitionistic logic in one direction, although some are theorems in both directions. Intuitionistic logic_sentence_52

They are as follows: Intuitionistic logic_sentence_53

Conjunction versus disjunction: Intuitionistic logic_sentence_54

Conjunction versus implication: Intuitionistic logic_sentence_55

Disjunction versus implication: Intuitionistic logic_sentence_56

Universal versus existential quantification: Intuitionistic logic_sentence_57

So, for example, "a or b" is a stronger propositional formula than "if not a, then b", whereas these are classically interchangeable. Intuitionistic logic_sentence_58

On the other hand, "not (a or b)" is equivalent to "not a, and also not b". Intuitionistic logic_sentence_59

If we include equivalence in the list of connectives, some of the connectives become definable from others: Intuitionistic logic_sentence_60

In particular, {∨, ↔, ⊥} and {∨, ↔, ¬} are complete bases of intuitionistic connectives. Intuitionistic logic_sentence_61

As shown by Alexander Kuznetsov, either of the following connectives – the first one ternary, the second one quinary – is by itself functionally complete: either one can serve the role of a sole sufficient operator for intuitionistic propositional logic, thus forming an analog of the Sheffer stroke from classical propositional logic: Intuitionistic logic_sentence_62

Semantics Intuitionistic logic_section_10

The semantics are rather more complicated than for the classical case. Intuitionistic logic_sentence_63

A model theory can be given by Heyting algebras or, equivalently, by Kripke semantics. Intuitionistic logic_sentence_64

Recently, a Tarski-like model theory was proved complete by Bob Constable, but with a different notion of completeness than classically. Intuitionistic logic_sentence_65

Unproved statements in intuitionistic logic are not given an intermediate truth value (as is sometimes mistakenly asserted). Intuitionistic logic_sentence_66

One can prove that such statements have no third truth value, a result dating back to Glivenko in 1928. Intuitionistic logic_sentence_67

Instead they remain of unknown truth value, until they are either proved or disproved. Intuitionistic logic_sentence_68

Statements are disproved by deducing a contradiction from them. Intuitionistic logic_sentence_69

Heyting algebra semantics Intuitionistic logic_section_11

In classical logic, we often discuss the truth values that a formula can take. Intuitionistic logic_sentence_70

The values are usually chosen as the members of a Boolean algebra. Intuitionistic logic_sentence_71

The meet and join operations in the Boolean algebra are identified with the ∧ and ∨ logical connectives, so that the value of a formula of the form A ∧ B is the meet of the value of A and the value of B in the Boolean algebra. Intuitionistic logic_sentence_72

Then we have the useful theorem that a formula is a valid proposition of classical logic if and only if its value is 1 for every valuation—that is, for any assignment of values to its variables. Intuitionistic logic_sentence_73

A corresponding theorem is true for intuitionistic logic, but instead of assigning each formula a value from a Boolean algebra, one uses values from an Heyting algebra, of which Boolean algebras are a special case. Intuitionistic logic_sentence_74

A formula is valid in intuitionistic logic if and only if it receives the value of the top element for any valuation on any Heyting algebra. Intuitionistic logic_sentence_75

It can be shown that to recognize valid formulas, it is sufficient to consider a single Heyting algebra whose elements are the open subsets of the real line R. In this algebra we have: Intuitionistic logic_sentence_76

where int(X) is the interior of X and X its complement. Intuitionistic logic_sentence_77

The last identity concerning A → B allows us to calculate the value of ¬A: Intuitionistic logic_sentence_78

With these assignments, intuitionistically valid formulas are precisely those that are assigned the value of the entire line. Intuitionistic logic_sentence_79

For example, the formula ¬(A ∧ ¬A) is valid, because no matter what set X is chosen as the value of the formula A, the value of ¬(A ∧ ¬A) can be shown to be the entire line: Intuitionistic logic_sentence_80

So the valuation of this formula is true, and indeed the formula is valid. Intuitionistic logic_sentence_81

But the law of the excluded middle, A ∨ ¬A, can be shown to be invalid by using a specific value of the set of positive real numbers for A: Intuitionistic logic_sentence_82

The interpretation of any intuitionistically valid formula in the infinite Heyting algebra described above results in the top element, representing true, as the valuation of the formula, regardless of what values from the algebra are assigned to the variables of the formula. Intuitionistic logic_sentence_83

Conversely, for every invalid formula, there is an assignment of values to the variables that yields a valuation that differs from the top element. Intuitionistic logic_sentence_84

No finite Heyting algebra has both these properties. Intuitionistic logic_sentence_85

Kripke semantics Intuitionistic logic_section_12

Main article: Kripke semantics Intuitionistic logic_sentence_86

Building upon his work on semantics of modal logic, Saul Kripke created another semantics for intuitionistic logic, known as Kripke semantics or relational semantics. Intuitionistic logic_sentence_87

Tarski-like semantics Intuitionistic logic_section_13

It was discovered that Tarski-like semantics for intuitionistic logic were not possible to prove complete. Intuitionistic logic_sentence_88

However, Robert Constable has shown that a weaker notion of completeness still holds for intuitionistic logic under a Tarski-like model. Intuitionistic logic_sentence_89

In this notion of completeness we are concerned not with all of the statements that are true of every model, but with the statements that are true in the same way in every model. Intuitionistic logic_sentence_90

That is, a single proof that the model judges a formula to be true must be valid for every model. Intuitionistic logic_sentence_91

In this case, there is not only a proof of completeness, but one that is valid according to intuitionistic logic. Intuitionistic logic_sentence_92

Relation to other logics Intuitionistic logic_section_14

Intuitionistic logic is related by duality to a paraconsistent logic known as Brazilian, anti-intuitionistic or dual-intuitionistic logic. Intuitionistic logic_sentence_93

The subsystem of intuitionistic logic with the FALSE axiom removed is known as minimal logic. Intuitionistic logic_sentence_94

Relation to many-valued logic Intuitionistic logic_section_15

Kurt Gödel's work involving many-valued logic showed in 1932 that intuitionistic logic is not a finite-valued logic. Intuitionistic logic_sentence_95

(See the section titled Heyting algebra semantics above for an infinite-valued logic interpretation of intuitionistic logic.) Intuitionistic logic_sentence_96

Relation to intermediate logics Intuitionistic logic_section_16

Any finite Heyting algebra which is not equivalent to a Boolean algebra defines (semantically) an intermediate logic. Intuitionistic logic_sentence_97

On the other hand, validity of formulae in pure intuitionistic logic is not tied to any individual Heyting algebra but relates to any and all Heyting algebras at the same time. Intuitionistic logic_sentence_98

Relation to modal logic Intuitionistic logic_section_17

Any formula of the intuitionistic propositional logic (IPC) may be translated into the normal modal logic S4 as follows: Intuitionistic logic_sentence_99

and it has been demonstrated that the translated formula is valid in the propositional modal logic S4 if and only if the original formula is valid in IPC. Intuitionistic logic_sentence_100

The above set of formulae are called the Gödel–McKinsey–Tarski translation. Intuitionistic logic_sentence_101

There is also an intuitionistic version of modal logic S4 called Constructive Modal Logic CS4. Intuitionistic logic_sentence_102

Lambda calculus Intuitionistic logic_section_18

There is an extended Curry–Howard isomorphism between IPC and simply-typed lambda calculus. Intuitionistic logic_sentence_103

See also Intuitionistic logic_section_19

Intuitionistic logic_unordered_list_0

Credits to the contents of this page go to the authors of the corresponding Wikipedia page: logic.