IMPLICATION AND ITERATED IMPLICATION

✍ Scribed by John Jones

• Publisher: John Wiley and Sons
• Year: 1983
• Tongue: English
• Weight: 689 KB
• Volume: 29
• Category: Article
• ISSN: 0044-3050
• DOI: 10.1002/malq.19830291006

✦ Synopsis

Let C be the implication functor of LUBASIEWICZ (see [ 2 j ) and let IjPQ = (CP)JQ,

JOHN JONES

R2. If T is as above, and P is a formula which does not contain any occurrences of the variable functor denoted by A or any occurrences of the propositional variables denoted by U and V , then if AATP is a correct formula, then P is a correct formula.

A complete formalisation of the K,-valued propositional calculus with C as the only primitive functor is given by the following four axiom schemes and one rule of procedure, where APQ =dfCCPQQ (see [3]). Ax 1. CPCQP; Ax2. CCPQCCQRCPR ; Ax 3. CAPQAQP ; Ax4. ACPQCQP.

MP.

We shall in future refer to this as the C-calculus.

If P and CPQ are correct formulae, then Q is a correct formula.

We make the following definitions F,?'lPiR = d f R , Z7: = [P,R = d t CP,,rf:lPiR (n = 1, 2 , . . .);