Paraconsistent logic

Last updated

Paraconsistent logic is an attempt at a logical system to deal with contradictions in a discriminating[ clarification needed ] 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.

Contents

Inconsistency-tolerant logics have been discussed since at least 1910 (and arguably much earlier, for example in the writings of Aristotle); [1] however, the term paraconsistent ("beside the consistent") was first coined in 1976, by the Peruvian philosopher Francisco Miró Quesada Cantuarias. [2] The study of paraconsistent logic has been dubbed paraconsistency, [3] which encompasses the school of dialetheism.

Definition

In classical logic (as well as intuitionistic logic and most other logics), contradictions entail everything. This feature, known as the principle of explosion or ex contradictione sequitur quodlibet (Latin, "from a contradiction, anything follows") [4] can be expressed formally as

1Premise
2 Conjunction elimination from 1
3 Disjunction introduction from 2
4 Conjunction elimination from 1
5 Disjunctive syllogism from 3 and 4

Which means: if P and its negation ¬P are both assumed to be true, then of the two claims P and (some arbitrary) A, at least one is true. Therefore, P or A is true. However, if we know that either P or A is true, and also that P is false (that ¬P is true) we can conclude that A, which could be anything, is true. Thus if a theory contains a single inconsistency, the theory is trivial – that is, it has every sentence as a theorem.

The characteristic or defining feature of a paraconsistent logic is that it rejects the principle of explosion. As a result, paraconsistent logics, unlike classical and other logics, can be used to formalize inconsistent but non-trivial theories.

Comparison with classical logic

The entailment relations of paraconsistent logics are propositionally weaker than classical logic; that is, they deem fewer propositional inferences valid. The point is that a paraconsistent logic can never be a propositional extension of classical logic, that is, propositionally validate every entailment that classical logic does. In some sense, then, paraconsistent logic is more conservative or cautious than classical logic. It is due to such conservativeness that paraconsistent languages can be more expressive than their classical counterparts including the hierarchy of metalanguages due to Alfred Tarski and others. According to Solomon Feferman: "natural language abounds with directly or indirectly self-referential yet apparently harmless expressions—all of which are excluded from the Tarskian framework." [5] This expressive limitation can be overcome in paraconsistent logic.

Motivation

A primary motivation for paraconsistent logic is the conviction that it ought to be possible to reason with inconsistent information in a controlled and discriminating way. The principle of explosion precludes this, and so must be abandoned. In non-paraconsistent logics, there is only one inconsistent theory: the trivial theory that has every sentence as a theorem. Paraconsistent logic makes it possible to distinguish between inconsistent theories and to reason with them.

Research into paraconsistent logic has also led to the establishment of the philosophical school of dialetheism (most notably advocated by Graham Priest), which asserts that true contradictions exist in reality, for example groups of people holding opposing views on various moral issues. [6] Being a dialetheist rationally commits one to some form of paraconsistent logic, on pain of otherwise embracing trivialism, i.e. accepting that all contradictions (and equivalently all statements) are true. [7] However, the study of paraconsistent logics does not necessarily entail a dialetheist viewpoint. For example, one need not commit to either the existence of true theories or true contradictions, but would rather prefer a weaker standard like empirical adequacy, as proposed by Bas van Fraassen. [8]

Philosophy

In classical logic Aristotle's three laws, namely, the excluded middle (p or ¬p), non-contradiction ¬ (p ∧ ¬p) and identity (p iff p), are regarded as the same, due to the inter-definition of the connectives. Moreover, traditionally contradictoriness (the presence of contradictions in a theory or in a body of knowledge) and triviality (the fact that such a theory entails all possible consequences) are assumed inseparable, granted that negation is available. These views may be philosophically challenged, precisely on the grounds that they fail to distinguish between contradictoriness and other forms of inconsistency.

On the other hand, it is possible to derive triviality from the 'conflict' between consistency and contradictions, once these notions have been properly distinguished. The very notions of consistency and inconsistency may be furthermore internalized at the object language level.

Tradeoffs

Paraconsistency involves tradeoffs. In particular, abandoning the principle of explosion requires one to abandon at least one of the following two principles: [9]

Disjunction introduction
Disjunctive syllogism

Both of these principles have been challenged.

One approach is to reject disjunction introduction but keep disjunctive syllogism and transitivity. In this approach, rules of natural deduction hold, except for disjunction introduction and excluded middle; moreover, inference A⊢B does not necessarily mean entailment A⇒B. Also, the following usual Boolean properties hold: double negation as well as associativity, commutativity, distributivity, De Morgan, and idempotence inferences (for conjunction and disjunction). Furthermore, inconsistency-robust proof of negation holds for entailment: (A⇒(B∧¬B))⊢¬A.

Another approach is to reject disjunctive syllogism. From the perspective of dialetheism, it makes perfect sense that disjunctive syllogism should fail. The idea behind this syllogism is that, if ¬ A, then A is excluded and B can be inferred from A ∨ B. However, if A may hold as well as ¬A, then the argument for the inference is weakened.

Yet another approach is to do both simultaneously. In many systems of relevant logic, as well as linear logic, there are two separate disjunctive connectives. One allows disjunction introduction, and one allows disjunctive syllogism. Of course, this has the disadvantages entailed by separate disjunctive connectives including confusion between them and complexity in relating them.

Furthermore, the rule of proof of negation (below) just by itself is inconsistency non-robust in the sense that the negation of every proposition can be proved from a contradiction.

Proof of Negation If , then

Strictly speaking, having just the rule above is paraconsistent because it is not the case that every proposition can be proved from a contradiction. However, if the rule double negation elimination () is added as well, then every proposition can be proved from a contradiction. Double negation elimination does not hold for intuitionistic logic.

Logic of Paradox

One example of paraconsistent logic is the system known as LP ("Logic of Paradox"), first proposed by the Argentinian logician Florencio González Asenjo in 1966 and later popularized by Priest and others. [10]

One way of presenting the semantics for LP is to replace the usual functional valuation with a relational one. [11] The binary relation relates a formula to a truth value: means that is true, and means that is false. A formula must be assigned at least one truth value, but there is no requirement that it be assigned at most one truth value. The semantic clauses for negation and disjunction are given as follows:

(The other logical connectives are defined in terms of negation and disjunction as usual.) Or to put the same point less symbolically:

(Semantic) logical consequence is then defined as truth-preservation:

if and only if is true whenever every element of is true.

Now consider a valuation such that and but it is not the case that . It is easy to check that this valuation constitutes a counterexample to both explosion and disjunctive syllogism. However, it is also a counterexample to modus ponens for the material conditional of LP. For this reason, proponents of LP usually advocate expanding the system to include a stronger conditional connective that is not definable in terms of negation and disjunction. [12]

As one can verify, LP preserves most other inference patterns that one would expect to be valid, such as De Morgan's laws and the usual introduction and elimination rules for negation, conjunction, and disjunction. Surprisingly, the logical truths (or tautologies) of LP are precisely those of classical propositional logic. [13] (LP and classical logic differ only in the inferences they deem valid.) Relaxing the requirement that every formula be either true or false yields the weaker paraconsistent logic commonly known as first-degree entailment (FDE). Unlike LP, FDE contains no logical truths.

LP is only one of many paraconsistent logics that have been proposed. [14] It is presented here merely as an illustration of how a paraconsistent logic can work.

Relation to other logics

One important type of paraconsistent logic is relevance logic. A logic is relevant if it satisfies the following condition:

if AB is a theorem, then A and B share a non-logical constant.

It follows that a relevance logic cannot have (p ∧ ¬p) → q as a theorem, and thus (on reasonable assumptions) cannot validate the inference from {p, ¬p} to q.

Paraconsistent logic has significant overlap with many-valued logic; however, not all paraconsistent logics are many-valued (and, of course, not all many-valued logics are paraconsistent). Dialetheic logics, which are also many-valued, are paraconsistent, but the converse does not hold. The ideal 3-valued paraconsistent logic given below becomes the logic RM3 when the contrapositive is added.

Intuitionistic logic allows A ∨ ¬A not to be equivalent to true, while paraconsistent logic allows A ∧ ¬A not to be equivalent to false. Thus it seems natural to regard paraconsistent logic as the "dual" of intuitionistic logic. However, intuitionistic logic is a specific logical system whereas paraconsistent logic encompasses a large class of systems. Accordingly, the dual notion to paraconsistency is called paracompleteness, and the "dual" of intuitionistic logic (a specific paracomplete logic) is a specific paraconsistent system called anti-intuitionistic or dual-intuitionistic logic (sometimes referred to as Brazilian logic, for historical reasons). [15] The duality between the two systems is best seen within a sequent calculus framework. While in intuitionistic logic the sequent

is not derivable, in dual-intuitionistic logic

is not derivable[ citation needed ]. Similarly, in intuitionistic logic the sequent

is not derivable, while in dual-intuitionistic logic

is not derivable. Dual-intuitionistic logic contains a connective # known as pseudo-difference which is the dual of intuitionistic implication. Very loosely, A # B can be read as "A but not B". However, # is not truth-functional as one might expect a 'but not' operator to be; similarly, the intuitionistic implication operator cannot be treated like "¬ (A ∧ ¬B)". Dual-intuitionistic logic also features a basic connective ⊤ which is the dual of intuitionistic ⊥: negation may be defined as ¬A = (⊤ # A)

A full account of the duality between paraconsistent and intuitionistic logic, including an explanation on why dual-intuitionistic and paraconsistent logics do not coincide, can be found in Brunner and Carnielli (2005).

These other logics avoid explosion: implicational propositional calculus, positive propositional calculus, equivalential calculus and minimal logic. The latter, minimal logic, is both paraconsistent and paracomplete (a subsystem of intuitionistic logic). The other three simply do not allow one to express a contradiction to begin with since they lack the ability to form negations.

An ideal three-valued paraconsistent logic

Here is an example of a three-valued logic which is paraconsistent and ideal as defined in "Ideal Paraconsistent Logics" by O. Arieli, A. Avron, and A. Zamansky, especially pages 22–23. [16] The three truth-values are: t (true only), b (both true and false), and f (false only).

P¬P
tf
bb
ft
P → QQ
tbf
Pttbf
btbf
fttt
P ∨ QQ
tbf
Ptttt
btbb
ftbf
P ∧ QQ
tbf
Pttbf
bbbf
ffff

A formula is true if its truth-value is either t or b for the valuation being used. A formula is a tautology of paraconsistent logic if it is true in every valuation which maps atomic propositions to {t, b, f}. Every tautology of paraconsistent logic is also a tautology of classical logic. For a valuation, the set of true formulas is closed under modus ponens and the deduction theorem. Any tautology of classical logic which contains no negations is also a tautology of paraconsistent logic (by merging b into t). This logic is sometimes referred to as "Pac" or "LFI1".

Included

Some tautologies of paraconsistent logic are:

** for deduction theorem and ?→{t,b} = {t,b}
** for deduction theorem (note: {t,b}→{f} = {f} follows from the deduction theorem)
** {f}→? = {t}
** ?→{t} = {t}
** {t,b}→{b,f} = {b,f}
** ~{f} = {t}
** ~{t,b} = {b,f} (note: ~{t} = {f} and ~{b,f} = {t,b} follow from the way the truth-values are encoded)
** {t,b}v? = {t,b}
** ?v{t,b} = {t,b}
** {t}v? = {t}
** ?v{t} = {t}
** {f}v{f} = {f}
** {b,f}v{b,f} = {b,f}
** {f}&? = {f}
** ?&{f} = {f}
** {b,f}&? = {b.f}
** ?&{b,f} = {b,f}
** {t}&{t} = {t}
** {t,b}&{t,b} = {t,b}
** ? is the union of {t,b} with {b,f}
** every truth-value is either t, b, or f.

Excluded

Some tautologies of classical logic which are not tautologies of paraconsistent logic are:

** no explosion in paraconsistent logic
** disjunctive syllogism fails in paraconsistent logic
** contrapositive fails in paraconsistent logic
** not all contradictions are equivalent in paraconsistent logic
** counter-factual for {b,f}→? = {t,b} (inconsistent with bf = f)

Strategy

Suppose we are faced with a contradictory set of premises Γ and wish to avoid being reduced to triviality. In classical logic, the only method one can use is to reject one or more of the premises in Γ. In paraconsistent logic, we may try to compartmentalize the contradiction. That is, weaken the logic so that ΓX is no longer a tautology provided the propositional variable X does not appear in Γ. However, we do not want to weaken the logic any more than is necessary for that purpose. So we wish to retain modus ponens and the deduction theorem as well as the axioms which are the introduction and elimination rules for the logical connectives (where possible).

To this end, we add a third truth-value b which will be employed within the compartment containing the contradiction. We make b a fixed point of all the logical connectives.

We must make b a kind of truth (in addition to t) because otherwise there would be no tautologies at all.

To ensure that modus ponens works, we must have

that is, to ensure that a true hypothesis and a true implication lead to a true conclusion, we must have that a not-true (f) conclusion and a true (t or b) hypothesis yield a not-true implication.

If all the propositional variables in Γ are assigned the value b, then Γ itself will have the value b. If we give X the value f, then

.

So ΓX will not be a tautology.

Limitations: (1) There must not be constants for the truth values because that would defeat the purpose of paraconsistent logic. Having b would change the language from that of classical logic. Having t or f would allow the explosion again because

or

would be tautologies. Note that b is not a fixed point of those constants since bt and bf.

(2) This logic's ability to contain contradictions applies only to contradictions among particularized premises, not to contradictions among axiom schemas.

(3) The loss of disjunctive syllogism may result in insufficient commitment to developing the 'correct' alternative, possibly crippling mathematics.

(4) To establish that a formula Γ is equivalent to Δ in the sense that either can be substituted for the other wherever they appear as a subformula, one must show

.

This is more difficult than in classical logic because the contrapositives do not necessarily follow.

Applications

Paraconsistent logic has been applied as a means of managing inconsistency in numerous domains, including: [17]

Criticism

Some philosophers have argued against dialetheism on the grounds that the counterintuitiveness of giving up any of the three principles above outweighs any counterintuitiveness that the principle of explosion might have.

Others, such as David Lewis, have objected to paraconsistent logic on the ground that it is simply impossible for a statement and its negation to be jointly true. [30] A related objection is that "negation" in paraconsistent logic is not really negation ; it is merely a subcontrary-forming operator. [31]

Alternatives

Approaches exist that allow for resolution of inconsistent beliefs without violating any of the intuitive logical principles. Most such systems use multi-valued logic with Bayesian inference and the Dempster-Shafer theory, allowing that no non-tautological belief is completely (100%) irrefutable because it must be based upon incomplete, abstracted, interpreted, likely unconfirmed, potentially uninformed, and possibly incorrect knowledge (of course, this very assumption, if non-tautological, entails its own refutability, if by "refutable" we mean "not completely [100%] irrefutable"). These systems effectively give up several logical principles in practice without rejecting them in theory.[ citation needed ]

Notable figures

Notable figures in the history and/or modern development of paraconsistent logic include:

See also

Notes

  1. "Paraconsistent Logic". Stanford Encyclopedia of Philosophy . Archived from the original on 2015-12-11. Retrieved 1 December 2015.
  2. Priest (2002), p. 288 and §3.3.
  3. Carnielli, W.; Rodrigues, A. "An epistemic approach to paraconsistency: a logic of evidence and truth" Pittsburg
  4. Carnielli, W. and Marcos, J. (2001) "Ex contradictione non sequitur quodlibet" Archived 2012-10-16 at the Wayback Machine Proc. 2nd Conf. on Reasoning and Logic (Bucharest, July 2000)
  5. Feferman, Solomon (1984). "Toward Useful Type-Free Theories, I". The Journal of Symbolic Logic. 49 (1): 75–111. doi:10.2307/2274093. JSTOR   2274093. S2CID   10575304.
  6. Jennifer Fisher (2007). On the Philosophy of Logic. Cengage Learning. pp. 132–134. ISBN   978-0-495-00888-0.
  7. Graham Priest (2007). "Paraconsistency and Dialetheism". In Dov M. Gabbay; John Woods (eds.). The Many Valued and Nonmonotonic Turn in Logic. Elsevier. p. 131. ISBN   978-0-444-51623-7.
  8. Otávio Bueno (2010). "Philosophy of Logic". In Fritz Allhoff (ed.). Philosophies of the Sciences: A Guide. John Wiley & Sons. p. 55. ISBN   978-1-4051-9995-7.
  9. See the article on the principle of explosion for more on this.
  10. Priest (2002), p. 306.
  11. LP is also commonly presented as a many-valued logic with three truth values (true, false, and both).
  12. See, for example, Priest (2002), §5.
  13. See Priest (2002), p. 310.
  14. Surveys of various approaches to paraconsistent logic can be found in Bremer (2005) and Priest (2002), and a large family of paraconsistent logics is developed in detail in Carnielli, Congilio and Marcos (2007).
  15. See Aoyama (2004).
  16. "Ideal Paraconsistent Logics" (PDF). Archived (PDF) from the original on 2017-08-09. Retrieved 2018-08-21.
  17. Most of these are discussed in Bremer (2005) and Priest (2002).
  18. See, for example, truth maintenance systems or the articles in Bertossi et al. (2004).
  19. Gershenson, C. (1999). Modelling emotions with multidimensional logic. In Proceedings of the 18th International Conference of the North American Fuzzy Information Processing Society (NAFIPS ’99), pp. 42–46, New York City, NY. IEEE Press. http://cogprints.org/1479/
  20. de Carvalho Junior, A.; Justo, J. F.; Angelico, B. A.; de Oliveira, A. M.; da Silva Filho, J. I. (2021). "Rotary Inverted Pendulum Identification for Control by Paraconsistent Neural Network". IEEE Access. 9: 74155–74167. Bibcode:2021IEEEA...974155D. doi: 10.1109/ACCESS.2021.3080176 . ISSN   2169-3536.
  21. Hewitt (2008b)
  22. Hewitt (2008a)
  23. Carl Hewitt. "Formalizing common sense reasoning for scalable inconsistency-robust information coordination using Direct Logic Reasoning and the Actor Model". in Vol. 52 of Studies in Logic. College Publications. ISBN   1848901593. 2015.
  24. de Carvalho Junior, Arnaldo; Justo, João Francisco; de Oliveira, Alexandre Maniçoba; da Silva Filho, João Inacio (1 January 2024). "A comprehensive review on paraconsistent annotated evidential logic: Algorithms, Applications, and Perspectives". Engineering Applications of Artificial Intelligence. 127 (B): 107342. doi:10.1016/j.engappai.2023.107342. S2CID   264898768.
  25. Carvalho, A.; Angelico, B. A.; Justo, J. F.; Oliveira, A. M.; Silva, J. I. D. (2023). "Model reference control by recurrent neural network built with paraconsistent neurons for trajectory tracking of a rotary inverted pendulum". Applied Soft Computing. 133: 109927. doi:10.1016/j.asoc.2022.109927. ISSN   1568-4946.
  26. de Carvalho Junior, Arnaldo; Justo, João Francisco; de Oliveira, Alexandre Maniçoba; da Silva Filho, João Inacio (1 January 2024). "A comprehensive review on paraconsistent annotated evidential logic: Algorithms, Applications, and Perspectives". Engineering Applications of Artificial Intelligence. 127 (B): 107342. doi:10.1016/j.engappai.2023.107342. S2CID   264898768.
  27. de Carvalho Jr., Arnaldo; Da Silva Filho, João Inácio; de Freitas Minicz, Márcio; Matuck, Gustavo R.; Côrtes, Hyghor Miranda; Garcia, Dorotéa Vilanova; Tasinaffo, Paulo Marcelo; Abe, Jair Minoro (2023). "A Paraconsistent Artificial Neural Cell of Learning by Contradiction Extraction (PANCLCTX) with Application Examples". Advances in Applied Logics. Intelligent Systems Reference Library. Vol. 243. pp. 63–79. doi:10.1007/978-3-031-35759-6_5. ISBN   978-3-031-35758-9.
  28. Carvalho, Arnaldo; Justo, João F.; Angélico, Bruno A.; de Oliveira, Alexandre M.; da Silva Filho, João Inacio (22 October 2022). "Paraconsistent State Estimator for a Furuta Pendulum Control". SN Computer Science. 4 (1). doi:10.1007/s42979-022-01427-z. S2CID   253064746.
  29. de Carvalho Junior, Arnaldo; Justo, João Francisco; de Oliveira, Alexandre Maniçoba; da Silva Filho, João Inacio (1 January 2024). "A comprehensive review on paraconsistent annotated evidential logic: Algorithms, Applications, and Perspectives". Engineering Applications of Artificial Intelligence. 127 (B): 107342. doi:10.1016/j.engappai.2023.107342. S2CID   264898768.
  30. See Lewis (1982).
  31. See Slater (1995), Béziau (2000).

Resources

Related Research Articles

In classical logic, disjunctive syllogism is a valid argument form which is a syllogism having a disjunctive statement for one of its premises.

<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, equivalence, and negation. Some sources include other connectives, as in the table below.

In logic, proof by contradiction is a form of proof that establishes the truth or the validity of a proposition, by showing that assuming the proposition to be false leads to a contradiction. Although it is quite freely used in mathematical proofs, not every school of mathematical thought accepts this kind of nonconstructive proof as universally valid.

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

In boolean logic, a disjunctive normal form (DNF) is a canonical normal form of a logical formula consisting of a disjunction of conjunctions; it can also be described as an OR of ANDs, a sum of products, or — in philosophical logic — a cluster concept. As a normal form, it is useful in automated theorem proving.

In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a canonical normal form, it is useful in automated theorem proving and circuit theory.

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

Dialetheism is the view that there are statements that are both true and false. More precisely, it is the belief that there can be a true statement whose negation is also true. Such statements are called "true contradictions", dialetheia, or nondualisms.

In classical logic, intuitionistic logic and similar logical systems, the principle of explosion, or the principle of Pseudo-Scotus, is the law according to which any statement can be proven from a contradiction. That is, from a contradiction, any proposition can be inferred; this is known as deductive explosion.

In mathematical logic, a tautology is a formula or assertion that is true in every possible interpretation. An example is "x=y or x≠y". Similarly, "either the ball is green, or the ball is not green" is always true, regardless of the colour of the ball.

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:

In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well.

In logic and mathematics, contraposition refers to the inference of going from a conditional statement into its logically equivalent contrapositive, and an associated proof method known as proof by contraposition. The contrapositive of a statement has its antecedent and consequent inverted and flipped.

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

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