Namespaces
Variants
Actions

Difference between revisions of "Positive propositional calculus"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
(TeX)
 
Line 1: Line 1:
A [[Propositional calculus|propositional calculus]] in the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p073/p073950/p0739501.png" /> specified by the following 8 axiom schemes:
+
{{TEX|done}}
 +
A [[Propositional calculus|propositional calculus]] in the language $\{\&,\lor,\supset\}$ specified by the following 8 axiom schemes:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p073/p073950/p0739502.png" /></td> </tr></table>
+
$$A\supset(B\supset A),\quad(A\supset(B\supset C))\supset((A\supset B)\supset(A\supset C)),$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p073/p073950/p0739503.png" /></td> </tr></table>
+
$$A\&B\supset A,\quad A\&B\supset B,\quad A\supset(B\supset A\&B),$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p073/p073950/p0739504.png" /></td> </tr></table>
+
$$A\supset A\lor B,\quad B\supset A\lor B,\quad(A\supset C)\supset((B\supset C)\supset(A\lor B)\supset C),$$
  
and the [[Modus ponens|modus ponens]] derivation rule. This calculus contains the part of the intuitionistic propositional calculus I (see [[Intuitionism|Intuitionism]]) that is not dependent on negation: Any propositional formula not containing <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p073/p073950/p0739505.png" /> (negation) is derivable in the positive propositional calculus if and only if it is derivable in I. One obtains the calculus I if one adds two axiom schemes to the positive propositional calculus:
+
and the [[Modus ponens|modus ponens]] derivation rule. This calculus contains the part of the intuitionistic propositional calculus I (see [[Intuitionism|Intuitionism]]) that is not dependent on negation: Any propositional formula not containing $\neg$ (negation) is derivable in the positive propositional calculus if and only if it is derivable in I. One obtains the calculus I if one adds two axiom schemes to the positive propositional calculus:
  
1) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p073/p073950/p0739506.png" /> (antecedent negation law),
+
1) $\neg A\supset(A\supset B)$ (antecedent negation law),
  
2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p073/p073950/p0739507.png" /> (reductio ad absurdum law).
+
2) $(A\supset B)\supset((A\supset\neg B)\supset\neg A)$ (reductio ad absurdum law).
  
 
To derive I, instead of 2) one can take the weaker scheme:
 
To derive I, instead of 2) one can take the weaker scheme:
  
2') <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p073/p073950/p0739508.png" /> (law of partial reductio ad absurdum).
+
2') $(A\supset\neg A)\supset\neg A$ (law of partial reductio ad absurdum).
  
 
See also [[Implicative propositional calculus|Implicative propositional calculus]].
 
See also [[Implicative propositional calculus|Implicative propositional calculus]].

Latest revision as of 08:00, 12 August 2014

A propositional calculus in the language $\{\&,\lor,\supset\}$ specified by the following 8 axiom schemes:

$$A\supset(B\supset A),\quad(A\supset(B\supset C))\supset((A\supset B)\supset(A\supset C)),$$

$$A\&B\supset A,\quad A\&B\supset B,\quad A\supset(B\supset A\&B),$$

$$A\supset A\lor B,\quad B\supset A\lor B,\quad(A\supset C)\supset((B\supset C)\supset(A\lor B)\supset C),$$

and the modus ponens derivation rule. This calculus contains the part of the intuitionistic propositional calculus I (see Intuitionism) that is not dependent on negation: Any propositional formula not containing $\neg$ (negation) is derivable in the positive propositional calculus if and only if it is derivable in I. One obtains the calculus I if one adds two axiom schemes to the positive propositional calculus:

1) $\neg A\supset(A\supset B)$ (antecedent negation law),

2) $(A\supset B)\supset((A\supset\neg B)\supset\neg A)$ (reductio ad absurdum law).

To derive I, instead of 2) one can take the weaker scheme:

2') $(A\supset\neg A)\supset\neg A$ (law of partial reductio ad absurdum).

See also Implicative propositional calculus.

References

[1] A. Church, "Introduction to mathematical logic" , 1 , Princeton Univ. Press (1956)
[2] D. Hilbert, P. Bernays, "Grundlagen der Mathematik" , 1–2 , Springer (1968–1970)
How to Cite This Entry:
Positive propositional calculus. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Positive_propositional_calculus&oldid=13329
This article was adapted from an original article by S.K. Sobolev (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article