minimal logic
   HOME

TheInfoList



OR:

Minimal logic, or minimal calculus, is a
symbolic logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
system originally developed by
Ingebrigt Johansson Ingebrigt Johansson. Ingebrigt Johansson (24 October 1904 in Narvik – 24 April 1987 in Oslo) was a Norwegian mathematician. He developed the symbolic logic system known as minimal logic Minimal logic, or minimal calculus, is a symbolic l ...
. It is an
intuitionistic In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of fu ...
and
paraconsistent logic A 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" syste ...
, that rejects both the
law of the excluded middle In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, Exclusive or, either this proposition or its negation is Truth value, true. It is one of the so-called Law of thought#The three tradit ...
as well as the
principle of explosion In classical logic, intuitionistic logic and similar logical systems, the principle of explosion (, 'from falsehood, anything ollows; or ), or the principle of Pseudo-Scotus, is the law according to which any statement can be proven from a co ...
(''ex falso quodlibet''), and therefore holding neither of the following two derivations as valid: :\vdash (B \lor \neg B) :(A \land \neg A) \vdash where A and B are any propositions. Most constructive logics only reject the former, the law of excluded middle. In classical logic, the ''ex falso'' laws :(A \land \neg A) \to B, :\neg(A \lor \neg A) \to B, :\neg A \to (A \to B), as well as their variants with A and \neg A switched, are equivalent to each other and valid. Minimal logic also rejects those principles.


Axiomatization

Minimal logic is axiomatized over the positive fragment of intuitionistic logic. These logics may be formulated in the language using implication \to,
conjunction Conjunction may refer to: * Conjunction (grammar), a part of speech * Logical conjunction, a mathematical operator ** Conjunction introduction, a rule of inference of propositional logic * Conjunction (astronomy), in which two astronomical bodies ...
\land and
disjunction In logic, disjunction is a logical connective typically notated as \lor and read aloud as "or". For instance, the English language sentence "it is raining or it is snowing" can be represented in logic using the disjunctive formula R \lor S ...
\lor as the basic
connectives In logic, a logical connective (also called a logical operator, sentential connective, or sentential operator) is a logical constant. They can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary co ...
, together with the adoption of falsum or absurdity \bot. Alternatively, direct axioms for negation are discussed below.


Theorems

Here only theorems not already provable in the positive calculus are covered.


Negation introduction

A quick analysis of implication and negation laws gives a good indication of what this logic, lacking full explosion, can and cannot prove. A natural statement in a language with
negation In logic, negation, also called the logical complement, is an operation that takes a proposition P to another proposition "not P", written \neg P, \mathord P or \overline. It is interpreted intuitively as being true when P is false, and false ...
, such as Minimal logic, is, for example, the principle of
negation introduction Negation introduction is a rule of inference, or transformation rule, in the field of propositional calculus. Negation introduction states that if a given antecedent implies both the consequent and its complement, then the antecedent is a contr ...
, whereby the negation of a statement is proven by assuming it and deriving a contradiction. Formally, this may be expressed as, for any two propositions, :(B\to (A\land \neg A))\to \neg B. For B taken as the contradiction A\land \neg A itself, this establishes the
law of non-contradiction In logic, the law of non-contradiction (LNC) (also known as the law of contradiction, principle of non-contradiction (PNC), or the principle of contradiction) states that contradictory propositions cannot both be true in the same sense at the sa ...
:\neg(A\land \neg A). Assuming any C, the introduction rule of the
material conditional The material conditional (also known as material implication) is an operation commonly used in logic. When the conditional symbol \rightarrow is interpreted as material implication, a formula P \rightarrow Q is true unless P is true and Q is ...
gives B\to C, also when B and C are not relevantly related. With this and implication elimination, the above introduction principle implies :(A\land \neg A)\to\neg B, i.e. assuming any contradiction, every proposition can be negated. Negation introduction is possible in minimal logic, so here a contradiction moreover proves every double negation \neg \neg B. Explosion would permit to remove the latter double negation, but this principle is not adopted. Moreover, using the above :\big((A \lor B)\land \neg A\big) \to \big((B\lor\neg B)\land\neg \neg B)\big). This is to be compared with the full
disjunctive syllogism In classical logic, disjunctive syllogism (historically known as ''modus tollendo ponens'' (MTP), Latin for "mode that affirms by denying") is a valid argument form which is a syllogism having a disjunctive statement for one of its premise ...
.


Axiomatization via absurdity

One possible scheme of extending the positive calculus to minimal logic is to treat \neg B as an implication, in which case the theorems from the implication calculus of a logic carry over to negation statements. To this end, \bot is introduced as a proposition, not provable unless the system is inconsistent, and negation \neg B is then treated as an abbreviation for B \to \bot. Constructively, \bot represents a proposition for which there can be no reason to believe it. The already discussed principles can then be from theorems over the positive fragment. Negation ''introduction'', spelled out in the previous section, is implied as a mere special case of :(B\to (A\land (A\to C)))\to (B\to C) when C=\bot. In this way, minimal logic can be characterized as a constructive logic just without negation ''elimination'' (a.k.a. explosion). The above can is proved via
modus ponens In propositional logic, ''modus ponens'' (; MP), also known as ''modus ponendo ponens'' (Latin for "method of putting by placing") or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference. ...
, which as a proposition reads :(A \land (A\to C))\to C and is indeed a special case of the above, when B is true. With the definition of negation through \bot, the modus ponens statement itself can in the same way again be specialized, and then establishes the non-contradiction principle, also already spelled out above. Indeed, all the common intuitionistic implications involving conjunctions of two propositions can be obtained, including the currying equivalence. For an example, it is worth emphasizing the important equivalence :((A\lor B)\to C)\leftrightarrow((A\to C)\land (B\to C)), expressing that those are two equivalent ways of the saying that both A and B imply C. Firstly, from it the familiar
De Morgan's laws In propositional logic and Boolean algebra, De Morgan's laws, also known as De Morgan's theorem, are a pair of transformation rules that are both valid rules of inference. They are named after Augustus De Morgan, a 19th-century British mathem ...
is obtained, :\neg(A\lor B)\leftrightarrow(\neg A\land\neg B). Secondly, using it to dissolve one implication from a disjunction as antecedent into two implications, it follows that :((B\lor(B\to C))\to C)\to C and this reduces to the double negation of excluded middle :\neg\neg(B\lor\neg B) By implication introduction, :C\to (B\to C) This also already implies \bot\to (B\to\bot) showing directly how assuming \bot in minimal logic proves all negations. This has spelled out above as well, but here may be shortened to :\bot\to \neg B. If absurdity is primitive, full explosion can also be stated as \bot\to B.


Axiomatization via more principles

From B\to ((B\to C)\to C) follows :B\to \neg\neg B Related to the negation introduction principle, from :(A\to B)\to((B\to C)\to(A\to C)). minimal logic proves the contraposition :(A\to B)\to(\neg B\to\neg A). The above principles have also been obtained using theorems from the positive calculus in combination with \bot. Adopting the above double negation principle together with the contraposition principle gives an alternative axiomatization of minimal logic over the positive positive fragment of intuitionistic logic.


Unprovable sentences

The tactic of generalizing \neg A to A\to C does not work to prove all classically valid statements involving double negations. Note that any schema of the syntactic shape (A\to C)\to B is too strong to be provable: If it were provable, then any true proposition C would prove any other proposition B. Now a variant of interest here is where A be replaced by (B\to C). It shows, possibly unsurprisingly, that the naive generalization of the
double negation elimination In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition ''A'' is logically equivalent to ''not (not ...
\neg \neg B\to B cannot be provable in this way. The proposition \neg\neg(B\lor \neg B) is a theorem of minimal logic, as is (A\land \neg A)\to \neg \neg B. Therefore, adopting the full double negation principle \neg\neg B\to B in minimal logic brings the calculus back to
classical logic Classical logic (or standard logic or Frege-Russell logic) is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy. Characteristics Each logical system in this class ...
, also skipping all
intermediate logic 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 l ...
s. There are also propositional logic statements that are unprovable in minimal logic, but do hold intuitionistically. With explosion for negated statements, full explosion is equivalent to its special case ((\neg B) \land \neg(\neg B))\to B. The latter can be phrased as double negation elimination for rejected propositions, \neg B \to(\neg \neg B\to B). This principle also immediately proves the full disjunctive syllogism. So this is a relatively weak schema leading to the stronger
intuitionistic logic 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 ...
. As seen above, the double negated excluded middle for any proposition is already provable in minimal logic. However, it is worth emphasizing that in the predicate calculus, the laws of minimal logic do not enable a proof of the double negation of an infinite conjunction of excluded middle statements. Indeed, the double negation shift schema (DNS) :\forall(n\in).\neg\neg P(n)\implies\neg\neg\forall(n\in). P(n) is not even intuitionistically valid and neither is \neg\neg\forall(n\in). Q(n)\lor\neg Q(n). Beyond
arithmetic Arithmetic () is an elementary part of mathematics that consists of the study of the properties of the traditional operations on numbers— addition, subtraction, multiplication, division, exponentiation, and extraction of roots. In the 19th ...
, this allows for non-classical theories.


Relation to intuitionistic logic

Any formula using only \land, \lor, \to is provable in minimal logic if and only if it is provable in intuitionistic logic. The principle of explosion is valid in intuitionistic logic and expresses that to derive any and all propositions, one may do this by deriving any absurdity. In minimal logic, this principle does not axiomatically hold for arbitrary propositions. As minimal logic represents only the positive fragment of intuitionistic logic, it is a subsystem of intuitionistic logic and is strictly weaker. Formulated concisely, explosion in intuitionistic logic exactly grants particular cases of the double negation elimination principle that minimal logic does not have.


Disjunctive syllogism

Practically, in the intuitionistic context, the principle of explosion enables the disjunctive syllogism: :((A \lor B)\land \neg A) \to B. This can be read as follows: Given a constructive proof of A \lor B and constructive rejection of A, one unconditionally allows for the positive case choice of B. In this way, the syllogism is an unpacking principle for the disjunction. It can be seen as a formal consequence of explosion and it also implies it. This is because if A \lor B was proven by proving B then B is already proven, while if A \lor B was proven by proving A, then B also follows, as the intuitionistic system allows for explosion. For example, given a constructive argument that a coin flip resulted in either heads or tails (A or B), together with a constructive argument that the outcome was in fact not heads, the syllogism expresses that then this already constitutes an argument that tails occurred. If the intuitionistic logic system is metalogically assumed consistent, the syllogism may be read as saying that a constructive demonstration of A\lor B and \neg A, in the absence of other non-logical axioms demonstrating B, actually contains a demonstration of B. In minimal logic, one cannot obtain a proof of B in this way. However, the same premise implies the double-negation of B, i.e. \neg\neg B. If the minimal logic system is metalogically assumed consistent, then that implication formula can be expressed by saying that B merely cannot be rejected. Weak forms of explosion prove the disjunctive syllogism and in the other direction, the instance of the syllogism with A=\neg B reads ((B \lor \neg B)\land \neg \neg B) \to B and is equivalent to the double negation elimination for propositions for which excluded middle holds :(B \lor \neg B)\to (\neg \neg B \to B). As the material conditional grants double-negation elimination for proven propositions, this is again equivalent to double negation elimination for rejected propositions.


Intuitionist example of use in a theory

The following
Heyting arithmetic In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano a ...
theorem allows for proofs of existence claims that cannot be proven, by means of this general result, without the explosion principle. The result is essentially a family of simple double negation elimination claims, \exists-sentences binding a computable predicate. Let P be any quantifier-free predicate, and thus decidable for all numbers n, so that excluded middle holds, :P(n)\lor\neg P(n). Then by induction in m, :\forall m.\ \neg\big(\forall(n In words: For the numbers n within a finite range up to m, if it can be ruled out that no case is validating, i.e. if it can be ruled out that for every number, say n=a, the corresponding proposition P(a) will always be disprovable, then this implies that there is some n=b among those n's for which P(b) is provable. As with examples discussed previously, a proof of this requires explosion on the antecedent side to obtain propositions without negations. If the proposition is formulated as starting at m=0, then this initial case already gives a form of explosion from a vacuous clause :\bot\to\exists(b<0). P(b). The next case m=1 states the double negation elimination for a decidable predicate, :\neg\neg P(0)\to P(0). The m=2 case reads :\neg\big(\neg P(0)\land \neg P(1)\big)\to \big(P(0)\lor P(1)\big), which, as already noted, is equivalent to :\neg\neg \big(P(0)\lor P(1)\big)\to \big(P(0)\lor P(1)\big). Both m=0 and m=1 are again cases of double negation elimination for a decidable predicate. Of course, a statement \exists(b for fixed m and P may be provable by other means, using principles of minimal logic. As an aside, the unbounded schema for general decidable predicates is not even intuitionistically provable, see
Markov's principle Markov's principle, named after Andrey Markov Jr, is a conditional existence statement for which there are many equivalent formulations, as discussed below. The principle is logically valid classically, but not in intuitionistic constructive m ...
.


Relation to type theory


Use of negation

Absurdity \bot is used not only in
natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axiom ...
, but also in type theoretical formulations under the
Curry–Howard correspondence In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relati ...
. In type systems, \bot is often also introduced as the empty type. In many contexts, \bot need not be a separate constant in the logic but its role can be replaced with any rejected proposition. For example, it can be defined as a=b where a, b ought to be distinct. The claim of non-existence of a proof for that proposition is then a claim of consistency. An example characterization for \bot is 0=1 in a theory involving natural numbers. This may also be adopted for in plain constructive logic. With this, proving 3^4=8 to be false, i.e. \neg(3^4=8), just means to prove (3^4=8)\to(0=1). We may introduce the notation 3^4 \neq 8 to capture the claim as well. And indeed, using arithmetic, \tfrac=1 holds, but (3^4=8) also implies \tfrac=0. So this would imply 1=0 and hence we obtain \neg(3^4=8). QED.


Simple types

Functional programming In computer science, functional programming is a programming paradigm where programs are constructed by Function application, applying and Function composition (computer science), composing Function (computer science), functions. It is a declar ...
calculi already foremostly depend on the implication connective, see e.g. the
calculus of constructions In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, ...
for a
predicate logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
framework. In this section we mention the system obtained by restricting minimal logic to implication only, and describe it formally. It can be defined by the following
sequent In mathematical logic, a sequent is a very general kind of conditional assertion. : A_1,\,\dots,A_m \,\vdash\, B_1,\,\dots,B_n. A sequent may have any number ''m'' of condition formulas ''Ai'' (called " antecedents") and any number ''n'' of asse ...
rules: :\dfrac \mbox         \dfrac \mbox         \dfrac \mbox Here: p.125, p.132 Each formula of this restricted minimal logic corresponds to a type in the
simply typed lambda calculus The simply typed lambda calculus (\lambda^\to), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda cal ...
, see
Curry–Howard correspondence In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relati ...
.


Semantics

There are semantics of minimal logic that mirror the frame-semantics of
intuitionistic logic 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 ...
, see the discussion of semantics in
paraconsistent logic A 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" syste ...
. Here the valuation functions assigning truth and falsity to propositions can be subject to fewer constraints.


See also

*
Intuitionistic logic 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 ...
*
Paraconsistent logic A 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" syste ...
*
Implicational propositional calculus In mathematical logic, the implicational propositional calculus is a version of classical propositional calculus which uses only one connective, called implication or conditional. In formulas, this binary operation is indicated by "implies", "if ...
*
List of logic systems This article contains a list of sample Hilbert-style deductive systems for propositional logics. Classical propositional calculus systems Classical propositional calculus is the standard propositional logic. Its intended semantics is bivalent ...


References

* A.S. Troelstra and H. Schwichtenberg, 2000, ''Basic Proof Theory'', Cambridge University Press, {{Logic Non-classical logic Constructivism (mathematics) Systems of formal logic