Minimal logic

Last updated

Minimal logic, or minimal calculus, is a symbolic logic system originally developed by Ingebrigt Johansson. [1] It is an intuitionistic and paraconsistent logic, that rejects both the law of the excluded middle as well as the principle of explosion (ex falso quodlibet), and therefore holding neither of the following two derivations as valid:

Contents

where and are any propositions. Most constructive logics only reject the former, the law of excluded middle. In classical logic, the ex falso laws

as well as their variants with and switched, are equivalent to each other and valid. Minimal logic also rejects those principles.

Note that the name has sometimes also been used to denote logic systems with a restricted number of connectives.

Axiomatization

Minimal logic is axiomatized over the positive fragment of intuitionistic logic. Both of these logics may be formulated in the language using the same axioms for implication , conjunction and disjunction as the basic connectives, but minimal logic conventionally adds falsum or absurdity as part of the language.

Other formulations are possible, of course all avoiding explosion. Direct axioms for negation are given below. A desideratum is always the negation introduction law, discussed next.

Theorems

Negation introduction

A quick analysis of the valid rules for negation gives a good preview of what this logic, lacking full explosion, can and cannot prove. A natural statement in a language with negation, such as minimal logic, is, for example, the principle of negation introduction, whereby the negation of a statement is proven by assuming the statement and deriving a contradiction. Over minimal logic, the principle is equivalent to

,

for any two propositions. For taken as the contradiction itself, this establishes the law of non-contradiction

.

Assuming any , the introduction rule of the material conditional gives , also when and are not relevantly related. With this and implication elimination, the above introduction principle implies

,

i.e. assuming any contradiction, every proposition can be negated. Negation introduction is possible in minimal logic, so here any contradiction moreover proves any double negation, . Explosion would permit to remove the latter double negation, but this principle is not adopted.

Axiomatization via absurdity

One possible scheme of extending the positive calculus to minimal logic is to treat as an implication, in which case the theorems from the constructive implication calculus of a logic carry over to negation statements. To this end, is introduced as a proposition, not provable unless the system is inconsistent, and negation is then treated as an abbreviation for . Constructively, represents a proposition for which there can be no reason to believe it.

Implications

As for the adopted principles in the implication calculus, which do not involve negations, the page on Hilbert system presents it through propositional forms of the axioms of law of identity, implication introduction and a variant of modus ponens. Note the equivalence proven there. For a first derivation, setting here at once results in the schema

.

In the intuitionistic Hilbert system, when not introducing as a constant, this can be taken as the second negation-characterizing axiom. (The other being explosion.)

Now, firstly, with taken as , this the above shows that

.

But, secondly, this short implication may also more directly be derived from modus ponens in the propositional form by considering .

Thirdly, it follows from the valid weak form of consequentia mirabilis: . In other words, a statement cannot be rejected exactly when the negation of the statement implies that it cannot be rejected. In particular, one may prove e.g. by proving .

Fourthly, the implication above also follows from

which is related to the double-negation principle. This theorem may be established from , by again reasoning with another variable very similar to the above, proving , and so on.

From the first theorem one further gets , and so

.

Generalizing some of the above in another way, one has . Under the Curry-Howard correspondence, this, as one example, is justified by the lambda expression . Modus ponens further then really implies the equivalence , from which now also follows in another way.

Finally, by implication introduction, , and this also already implies showing directly how assuming in minimal logic proves all negations. It may be expressed as

If absurdity is primitive, full explosion principle could likewise also be stated as .

Conjunctions

Going beyond statements solely in terms of implications, the principles discussed previously can now also be established as theorems: With the definition of negation through , the modus ponens statement in the form itself specializes to the non-contradiction principle, when considering . When negation is an implication, then the curried form of non-contradiction is again . Further, negation introduction in the form with a conjunction, spelled out in the previous section, is implied as the mere special case of

In this way, minimal logic can be characterized as a constructive logic just without negation elimination (a.k.a. explosion).

With this, most of the common intuitionistic implications involving conjunctions of two propositions can be obtained, including the currying equivalence.

Disjunctions

It is worth emphasizing the important equivalence

,

expressing that those are two equivalent ways of the saying that both and imply . From it, two of the familiar De Morgan's laws are obtained,

.

The third valid De Morgan's law may also be derived.

The negation of an excluded middle statement implies its own validity. With reference to the weak variant of consequentia mirabilis above, it thus follows that

This result may also be seen as a special case of , which follows from when considering for .

Finally, case analysis shows

This implication is to be compared with the full disjunctive syllogism, discussed in detail below.

Axiomatization via alternative principles

Another theorem only involving implications shall be noted: Related to the negation introduction principle, from

.

minimal logic proves the contraposition

,

which like negation introduction again proves . All the above principles can be obtained using theorems from the positive calculus in combination with the constant .

Instead of the formulation with that constant, one may adopt as axioms the contraposition principle just stated, together with the double negation principle . This gives an alternative axiomatization of minimal logic over the positive fragment of intuitionistic logic.

Relation to classical logic

The tactic of generalizing to does not work to prove all classically valid statements involving double negations. In particular, unsurprisingly, the naive generalization of the double negation elimination cannot be provable in this way. Indeed whatever looks like, any schema of the syntactic form would be too strong: Considering any true proposition for makes this equivalent to just .

The proposition is a theorem of minimal logic, as is . Therefore, adopting the full double negation principle in minimal logic actually also proves explosion, and so brings the calculus back to classical logic, also skipping all intermediate logics.

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, not even the laws of the strictly stronger intuitionistic logic enable a proof of the double negation of an infinite conjunction of excluded middle statements. Indeed,

In turn, the double negation shift schema (DNS) is not valid either, that is

Beyond arithmetic, this unprovability allows for the axiomatization of non-classical theories.

Relation to paraconsistent logic

Minimal logic proves weaker variants of consequentia mirabilis, as demonstrated in that article. The full principle is, however, equivalent to excluded middle.

Relation to intuitionistic logic

Any formula using only is provable in minimal logic if and only if it is provable in intuitionistic logic. But there are also propositional logic statements that are unprovable in minimal logic, but do hold intuitionistically.

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.

With explosion for negated statements, full explosion is equivalent to its special case . The latter can be phrased as double negation elimination for rejected propositions, . Formulated concisely, explosion in intuitionistic logic exactly grants particular cases of the double negation elimination principle that minimal logic does not have. This principle also immediately proves the full disjunctive syllogism.

Disjunctive syllogism

Practically, in the intuitionistic context, the principle of explosion enables the disjunctive syllogism:

This can be read as follows: Given a constructive proof of and constructive rejection of , one unconditionally allows for the positive case choice of . 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 was proven by proving then is already proven, while if was proven by proving , then 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 ( or ), 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 and , in the absence of other non-logical axioms demonstrating , actually contains a demonstration of .

In minimal logic, one cannot obtain a proof of in this way. However, the same premise implies the double-negation of , i.e. . If the minimal logic system is metalogically assumed consistent, then that implication formula can be expressed by saying that merely cannot be rejected.

Weak forms of explosion prove the disjunctive syllogism and in the other direction, the instance of the syllogism with reads and is equivalent to the double negation elimination for propositions for which excluded middle holds

.

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 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, -sentences binding a computable predicate.

Let be any quantifier-free predicate, and thus decidable for all numbers , so that excluded middle holds,

.

Then by induction in ,

In words: For the numbers within a finite range up to , if it can be ruled out that no case is validating, i.e. if it can be ruled out that for every number, say , the corresponding proposition will always be disprovable, then this implies that there is some among those 's for which 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 , then this initial case already gives a form of explosion from a vacuous clause

.

The next case states the double negation elimination for a decidable predicate,

.

The case reads

,

which, as already noted, is equivalent to

.

Both and are again cases of double negation elimination for a decidable predicate. Of course, a statement for fixed and 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.

Relation to type theory

Use of negation

Absurdity is used not only in natural deduction, but also in type theoretical formulations under the Curry–Howard correspondence. In type systems, is often also introduced as the empty type.

In many contexts, 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 where 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 is in a theory involving natural numbers. This may also be adopted for in plain constructive logic. With this, proving to be false, i.e. , just means to prove . We may introduce the notation to capture the claim as well. And indeed, using arithmetic, holds, but also implies . So this would imply and hence we obtain . QED.

Simple types

Functional programming calculi already foremostly depend on the implication connective, see e.g. the calculus of constructions for a predicate logic 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 rules:

         [2] [3]

Each formula of this restricted minimal logic corresponds to a type in the simply typed lambda calculus, see Curry–Howard correspondence. In that context, the phrase minimal logic is sometimes used to mean this restriction of minimal logic. [4] This implicational fragment of minimal logic is the same as the positive, implicational fragment of intuitionistic logic since minimal Logic is already simply the positive fragment of intuitionistic logic.

Semantics

There are semantics of minimal logic that mirror the frame-semantics of intuitionistic logic, see the discussion of semantics in paraconsistent logic. Here the valuation functions assigning truth and falsity to propositions can be subject to fewer constraints.

See also

Notes

Related Research Articles

<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">De Morgan's laws</span> Pair of logical equivalences

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 mathematician. The rules allow the expression of conjunctions and disjunctions purely in terms of each other via negation.

<span class="mw-page-title-main">Contradiction</span> Logical incompatibility between two or more propositions

In traditional logic, a contradiction occurs when a proposition conflicts either with itself or established fact. It is often used as a tool to detect disingenuous beliefs and bias. Illustrating a general tendency in applied logic, Aristotle's law of noncontradiction states that "It is impossible that the same thing can at the same time both belong and not belong to the same object and in the same respect."

<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 propositional logic, the double negation of a statement states that "it is not the case that the statement is not true". In classical logic, every statement is logically equivalent to its double negation, but this is not true in intuitionistic logic; this can be expressed by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign ~ expresses negation.

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.

In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.

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 mathematics, a set is inhabited if there exists an element .

Consequentia mirabilis, also known as Clavius's Law, is used in traditional and classical logic to establish the truth of a proposition from the inconsistency of its negation. It is thus related to reductio ad absurdum, but it can prove a proposition using just its own negation and the concept of consistency. For a more concrete formulation, it states that if a proposition is a consequence of its negation, then it is true, for consistency. In formal notation:

Markov's principle, named after Andrey Markov Jr, is a conditional existence statement for which there are many equivalent formulations, as discussed below.

In constructive mathematics, Church's thesis is the principle stating that all total functions are computable functions.

In constructive mathematics, pseudo-order is a name given to certain binary relations appropriate for modeling continuous orderings.

<span class="mw-page-title-main">Peirce's law</span> Axiom used in logic and philosophy

In logic, Peirce's law is named after the philosopher and logician Charles Sanders Peirce. It was taken as an axiom in his first axiomatisation of propositional logic. It can be thought of as the law of excluded middle written in a form that involves only one sort of connective, namely implication.

A non-normal modal logic is a variant of modal logic that deviates from the basic principles of normal modal logics.

References