Many-valued logics

Sequent Calculus

Equation form expr-01208e159d2aec8c

∧\land

Read as: conjunction

Means: conjunction

2 occurrences in this chapter

Equation form expr-012adb5a2c26ae0b

B⇒!B \fCenter

Read as: the two sided sequent with antecedent formula B and succedent empty

Means: the two sided sequent with antecedent formula B and succedent empty

1 occurrence in this chapter

Equation form expr-021efa283e1aaf83

∧F\iR{\land}{\False}

Read as: conjunction rule at position false

Means: conjunction rule at position false

1 occurrence in this chapter

Equation form expr-04b0b77ebf59e09f

A∣…∣A!A \nSequent \dots \nSequent !A

Read as: the n sided sequent with formula A alone in every position

Means: the n sided sequent with formula A alone in every position

1 occurrence in this chapter

Equation form expr-073ec9d3ecd7fa0d

Γ∣B,Π∣B,Δ\Gamma \nSequent !B, \Pi \nSequent !B, \Delta

Read as: the three sided sequent with false position Gamma; middle position formula B, followed by Pi; and true position formula B, followed by Delta

Means: the three sided sequent with false position Gamma; middle position formula B, followed by Pi; and true position formula B, followed by Delta

1 occurrence in this chapter

Equation form expr-07871ab6298345c9

∨F\iR\lor\False

Read as: disjunction rule at position false

Means: disjunction rule at position false

1 occurrence in this chapter

Equation form expr-09bfc832719222a5

Π\Pi

Read as: Pi

Means: Pi

1 occurrence in this chapter

Equation form expr-0a231eaa20f13713

Γ0′\Gamma_0'

Read as: Gamma sub zero prime

Means: Gamma sub zero prime

2 occurrences in this chapter

Equation form expr-0d7eca7837fbd874

A⇒B!A \fCenter !B

Read as: the two sided sequent with antecedent formula A and succedent formula B

Means: the two sided sequent with antecedent formula A and succedent formula B

1 occurrence in this chapter

Equation form expr-0e7ee86646fb870d

A∧B,Γ∣Π∣Δ!A \land !B, \Gamma \nSequent \Pi \nSequent \Delta

Read as: the three sided sequent with false position the conjunction of formulas A and B, followed by Gamma; middle position Pi; and true position Delta

Means: the three sided sequent with false position the conjunction of formulas A and B, followed by Gamma; middle position Pi; and true position Delta

1 occurrence in this chapter

Equation form expr-0f1fa683f7157a3b

A∣A→B,A∣B,AA \nSequent A \lif B, A \nSequent B, A

Read as: the three sided sequent with false position formula A; middle position the conditional from formula A to formula B, followed by formula A; and true position formula B, followed by formula A

Means: the three sided sequent with false position formula A; middle position the conditional from formula A to formula B, followed by formula A; and true position formula B, followed by formula A

1 occurrence in this chapter

Equation form expr-12a82e1290b4207c

Γ∣Γ∣A\Gamma \nSequent \Gamma \nSequent !A

Read as: with Gamma in the false position, Gamma in the middle position, and A in the true position

Means: with Gamma in the false position, Gamma in the middle position, and A in the true position

1 occurrence in this chapter

Equation form expr-1321e86f9c85baba

Γ⊢LA\Gamma \Proves[\Log{L}] !A

Read as: formula A is derivable from Gamma in logic L

Means: formula A is derivable from Gamma in logic L

1 occurrence in this chapter

Equation form expr-13ef58934b3d908a

A→B,A∣A→B,A∣BA \lif B, A \nSequent A \lif B, A \nSequent B

Read as: the three sided sequent with false position the conditional from formula A to formula B, followed by formula A; middle position the conditional from formula A to formula B, followed by formula A; and true position formula B

Means: the three sided sequent with false position the conditional from formula A to formula B, followed by formula A; middle position the conditional from formula A to formula B, followed by formula A; and true position formula B

1 occurrence in this chapter

Equation form expr-16f38629e1f81ade

Ł3\LogLuk[3]

Read as: three valued Lukasiewicz logic

Means: three valued Lukasiewicz logic

1 occurrence in this chapter

Equation form expr-173333e0dd0c9bff

A,B,Γ⇒Δ!A, !B, \Gamma \fCenter \Delta

Read as: the two sided sequent with antecedent formula A, followed by formula B, followed by Gamma and succedent Delta

Means: the two sided sequent with antecedent formula A, followed by formula B, followed by Gamma and succedent Delta

1 occurrence in this chapter

Equation form expr-17c2ad44eafe9b91

A∨B,Γ∣Π∣Δ!A \lor !B, \Gamma \nSequent \Pi \nSequent \Delta

Read as: the three sided sequent with false position the disjunction of formulas A and B, followed by Gamma; middle position Pi; and true position Delta

Means: the three sided sequent with false position the disjunction of formulas A and B, followed by Gamma; middle position Pi; and true position Delta

1 occurrence in this chapter

Equation form expr-17d4eba6ad88ec82

→G3U\iR\lif\Undef[\LogGod[3]]

Read as: conditional rule at position middle in three valued Goedel logic

Means: conditional rule at position middle in three valued Goedel logic

1 occurrence in this chapter

Equation form expr-19457f21bbc58a7b

Γ∣A,Π∣Δ\Gamma \nSequent !A, \Pi \nSequent \Delta

Read as: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position Delta

Means: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position Delta

1 occurrence in this chapter

Equation form expr-1a72645069198d72

v¯(B)=T\pValue v(!B) = \True

Read as: the value of formula B under valuation v is true

Means: the value of formula B under valuation v is true

1 occurrence in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: n

13 occurrences in this chapter

Equation form expr-1c68f0ec31b7c8da

Ci\iR{\Contraction}{i}

Read as: contraction rule at position i

Means: contraction rule at position i

1 occurrence in this chapter

Equation form expr-1dcebf36422cadc4

B,A∣A,B,A∣BB, A \nSequent A, B, A \nSequent B

Read as: the three sided sequent with false position formula B, followed by formula A; middle position formula A, followed by formula B, followed by formula A; and true position formula B

Means: the three sided sequent with false position formula B, followed by formula A; middle position formula A, followed by formula B, followed by formula A; and true position formula B

1 occurrence in this chapter

Equation form expr-22bde50dea1cddc0

Γ∣Π∣Δ,A,B\Gamma \nSequent \Pi \nSequent \Delta, !A, !B

Read as: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A, followed by formula B

Means: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A, followed by formula B

1 occurrence in this chapter

Equation form expr-240313d5e995741c

v\pAssign{v}

Read as: v

Means: v

1 occurrence in this chapter

Equation form expr-284c47be48fb0c66

¬\lnot

Read as: negation

Means: negation

3 occurrences in this chapter

Equation form expr-289b7dbf1fcd3af9

Γ∣A,B,Π∣Δ\Gamma \nSequent !A, !B, \Pi \nSequent \Delta

Read as: the three sided sequent with false position Gamma; middle position formula A, followed by formula B, followed by Pi; and true position Delta

Means: the three sided sequent with false position Gamma; middle position formula A, followed by formula B, followed by Pi; and true position Delta

4 occurrences in this chapter

Equation form expr-28d551f1836f0e19

v¯(A)=F\pValue{v}(!A) = \False

Read as: the value of formula A under valuation v is false

Means: the value of formula A under valuation v is false

2 occurrences in this chapter

Equation form expr-2983166c4c2fdefe

(¯A)=F\pValue(!A) = \False

Read as: the source writes the value of formula A equals false, with the valuation argument omitted

Means: the source writes the value of formula A equals false, with the valuation argument omitted

1 occurrence in this chapter

Equation form expr-360ea1d7238635d3

Γ∣Π∣Δ,A\Gamma \nSequent \Pi \nSequent \Delta, !A

Read as: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A

Means: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A

5 occurrences in this chapter

Equation form expr-362138992adfe804

⋆\star

Read as: star

Means: star

2 occurrences in this chapter

Equation form expr-36c81da440012591

→KsT\iR{\lif}{\True}[\LogKs]

Read as: conditional rule at position true in strong Kleene logic

Means: conditional rule at position true in strong Kleene logic

1 occurrence in this chapter

Equation form expr-3ab24589d3ccef82

⇒A→B\fCenter !A \lif !B

Read as: the two sided sequent with antecedent empty and succedent the conditional from formula A to formula B

Means: the two sided sequent with antecedent empty and succedent the conditional from formula A to formula B

1 occurrence in this chapter

Equation form expr-3ae8814bcfcf3427

A∣B,A∣B,AA \nSequent B, A \nSequent B, A

Read as: the three sided sequent with false position formula A; middle position formula B, followed by formula A; and true position formula B, followed by formula A

Means: the three sided sequent with false position formula A; middle position formula B, followed by formula A; and true position formula B, followed by formula A

1 occurrence in this chapter

Equation form expr-3bb1d7b8be82b9c4

Γ∣Π∣Δ\Gamma \mid \Pi \mid \Delta

Read as: with Gamma in the false position, Pi in the middle position, and Delta in the true position

Means: with Gamma in the false position, Pi in the middle position, and Delta in the true position

1 occurrence in this chapter

Equation form expr-3c1d99241eb50a41

→KsU\iR\lif\Undef[\LogKs]

Read as: conditional rule at position middle in strong Kleene logic

Means: conditional rule at position middle in strong Kleene logic

1 occurrence in this chapter

Equation form expr-3c859dea115e4157

A,B∣A,B,A∣BA, B \nSequent A, B, A \nSequent B

Read as: the three sided sequent with false position formula A, followed by formula B; middle position formula A, followed by formula B, followed by formula A; and true position formula B

Means: the three sided sequent with false position formula A, followed by formula B; middle position formula A, followed by formula B, followed by formula A; and true position formula B

1 occurrence in this chapter

Equation form expr-3dbd7e5314541fec

A∣A,B,A∣B,AA \nSequent A, B, A \nSequent B, A

Read as: the three sided sequent with false position formula A; middle position formula A, followed by formula B, followed by formula A; and true position formula B, followed by formula A

Means: the three sided sequent with false position formula A; middle position formula A, followed by formula B, followed by formula A; and true position formula B, followed by formula A

1 occurrence in this chapter

Equation form expr-3e1951fe2e90b552

Γ⊢Ł3A\Gamma \Proves[\LogLuk[3]] !A

Read as: formula A is derivable from Gamma in three valued Lukasiewicz logic

Means: formula A is derivable from Gamma in three valued Lukasiewicz logic

1 occurrence in this chapter

Equation form expr-3f8a5b83f471d97d

Γ∣¬A,Π∣Δ\Gamma \nSequent \lnot !A, \Pi \nSequent \Delta

Read as: the three sided sequent with false position Gamma; middle position the negation of formula A, followed by Pi; and true position Delta

Means: the three sided sequent with false position Gamma; middle position the negation of formula A, followed by Pi; and true position Delta

1 occurrence in this chapter

Equation form expr-428b541183d09d07

A,Γ∣B,Π∣Δ,B!A, \Gamma \nSequent !B, \Pi \nSequent \Delta, !B

Read as: the three sided sequent with false position formula A, followed by Gamma; middle position formula B, followed by Pi; and true position Delta, followed by formula B

Means: the three sided sequent with false position formula A, followed by Gamma; middle position formula B, followed by Pi; and true position Delta, followed by formula B

2 occurrences in this chapter

Equation form expr-494bbeea7642cd26

Λi\Lambda_i

Read as: Lambda sub i

Means: Lambda sub i

1 occurrence in this chapter

Equation form expr-49eb0cd106d1aa6b

→R\RightR{\lif}

Read as: right conditional rule

Means: right conditional rule

1 occurrence in this chapter

Equation form expr-4bd1816df0cb6e4e

→G3T\iR{\lif}{\True}[\LogGod[3]]

Read as: conditional rule at position true in three valued Goedel logic

Means: conditional rule at position true in three valued Goedel logic

1 occurrence in this chapter

Equation form expr-4d71fd41650493cb

Γ∣A∣A\Gamma \nSequent !A \nSequent !A

Read as: the three sided sequent with false position Gamma; middle position formula A; and true position formula A

Means: the three sided sequent with false position Gamma; middle position formula A; and true position formula A

1 occurrence in this chapter

Equation form expr-4e07408562bedb8b

33

Read as: three

Means: three

3 occurrences in this chapter

Equation form expr-51ef1d1d214e9154

∧L\LeftR{\land}

Read as: left conjunction

Means: left conjunction

1 occurrence in this chapter

Equation form expr-52073e0f6d8c837f

A∣A∣B,AA \nSequent A \nSequent B, A

Read as: the three sided sequent with false position formula A; middle position formula A; and true position formula B, followed by formula A

Means: the three sided sequent with false position formula A; middle position formula A; and true position formula B, followed by formula A

2 occurrences in this chapter

Equation form expr-529ad2daacd7efcb

∨\lor

Read as: disjunction

Means: disjunction

2 occurrences in this chapter

Equation form expr-52ada128dd5c1f22

Γ∣Π∣Δ,B\Gamma \nSequent \Pi \nSequent \Delta, !B

Read as: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula B

Means: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula B

1 occurrence in this chapter

Equation form expr-556347ae74e2172b

v¯(A→B)=F\pValue v(!A \lif !B) = \False

Read as: the value of the conditional from A to B under valuation v is false

Means: the value of the conditional from A to B under valuation v is false

1 occurrence in this chapter

Equation form expr-55f5124bd9708425

A→B,Γ∣Π∣Δ!A \lif !B, \Gamma \nSequent \Pi \nSequent \Delta

Read as: the three sided sequent with false position the conditional from formula A to formula B, followed by Gamma; middle position Pi; and true position Delta

Means: the three sided sequent with false position the conditional from formula A to formula B, followed by Gamma; middle position Pi; and true position Delta

3 occurrences in this chapter

Equation form expr-560a56f26a90c784

A,Γ∣A,Π∣Δ,B!A, \Gamma \nSequent !A, \Pi \nSequent \Delta, !B

Read as: the three sided sequent with false position formula A, followed by Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula B

Means: the three sided sequent with false position formula A, followed by Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula B

2 occurrences in this chapter

Equation form expr-57885e4c75965b23

Γ\Gamma

Read as: Gamma

Means: Gamma

4 occurrences in this chapter

Equation form expr-59b1e5ec7d34df05

A∣A∣A,AA \nSequent A \nSequent A, A

Read as: the three sided sequent with false position formula A; middle position formula A; and true position formula A, followed by formula A

Means: the three sided sequent with false position formula A; middle position formula A; and true position formula A, followed by formula A

1 occurrence in this chapter

Equation form expr-59bb24ebe07ea335

Γ1∣…∣Γn\Gamma_1 \nSequent \dots \nSequent \Gamma_n

Read as: the n sided sequent whose positions, in order, contain Gamma sub one through Gamma sub n

Means: the n sided sequent whose positions, in order, contain Gamma sub one through Gamma sub n

1 occurrence in this chapter

Equation form expr-59cf7cd4fdb9ff5b

T\True

Read as: the true truth value

Means: the true truth value

2 occurrences in this chapter

Equation form expr-5cee14f183831f78

→G3F\iR\lif\False[\LogGod[3]]

Read as: conditional rule at position false in three valued Goedel logic

Means: conditional rule at position false in three valued Goedel logic

1 occurrence in this chapter

Equation form expr-5feceb66ffc86f38

00

Read as: zero

Means: zero

1 occurrence in this chapter

Equation form expr-618109b2dd73e181

B∣A,B,A∣BB \nSequent A, B, A \nSequent B

Read as: the three sided sequent with false position formula B; middle position formula A, followed by formula B, followed by formula A; and true position formula B

Means: the three sided sequent with false position formula B; middle position formula A, followed by formula B, followed by formula A; and true position formula B

1 occurrence in this chapter

Equation form expr-633ed2a1f4bb86d3

A∣A∣A!A \nSequent !A \nSequent !A

Read as: all three sided sequents with formula A in every position

Means: all three sided sequents with formula A in every position

1 occurrence in this chapter

Equation form expr-64d0f2c008a7c881

LK\Log{LK}

Read as: the classical sequent calculus L K

Means: the classical sequent calculus L K

1 occurrence in this chapter

Equation form expr-64dd9ec086ad4f5b

U\Undef

Read as: the middle truth value

Means: the middle truth value

3 occurrences in this chapter

Equation form expr-658dabfaad2a53bc

⇒A\fCenter !A

Read as: the two sided sequent with antecedent empty and succedent formula A

Means: the two sided sequent with antecedent empty and succedent formula A

1 occurrence in this chapter

Equation form expr-697b5c71bc6621ac

∨U\iR\lor\Undef

Read as: disjunction rule at position middle

Means: disjunction rule at position middle

1 occurrence in this chapter

Equation form expr-6db82c1ae3dfffcd

Γ1\Gamma_1

Read as: Gamma sub one

Means: Gamma sub one

1 occurrence in this chapter

Equation form expr-6de6064447e642ac

Γ⇒Δ,A∨B\Gamma \fCenter \Delta, !A \lor !B

Read as: the two sided sequent with antecedent Gamma and succedent Delta, followed by the disjunction of formulas A and B

Means: the two sided sequent with antecedent Gamma and succedent Delta, followed by the disjunction of formulas A and B

1 occurrence in this chapter

Equation form expr-708bcdb95379aeab

Γ1∣…∣Γi,B,A,Γi′∣…∣Γn\Gamma_1 \nSequent \dots \nSequent \Gamma_i, !B, !A, \Gamma_i' \nSequent \dots \nSequent \Gamma_n

Read as: the n sided sequent with position i containing Gamma sub i, formula B, formula A, then Gamma sub i prime; all other positions retain their respective Gamma sequences

Means: the n sided sequent with position i containing Gamma sub i, formula B, formula A, then Gamma sub i prime; all other positions retain their respective Gamma sequences

1 occurrence in this chapter

Equation form expr-73ea587851a6379b

A∣A∣AA \nSequent A \nSequent A

Read as: the three sided sequent with false position formula A; middle position formula A; and true position formula A

Means: the three sided sequent with false position formula A; middle position formula A; and true position formula A

3 occurrences in this chapter

Equation form expr-77d613281dda9ca4

V={F,U,T}V = \{\False, \Undef, \True\}

Read as: V equal to the set containing the false, middle, and true truth values

Means: V equal to the set containing the false, middle, and true truth values

1 occurrence in this chapter

Equation form expr-7826434dea345430

→L\LeftR{\lif}

Read as: left conditional rule

Means: left conditional rule

1 occurrence in this chapter

Equation form expr-7984c08bd9bb9465

B,A∣A→B,A∣BB, A \nSequent A \lif B, A \nSequent B

Read as: the three sided sequent with false position formula B, followed by formula A; middle position the conditional from formula A to formula B, followed by formula A; and true position formula B

Means: the three sided sequent with false position formula B, followed by formula A; middle position the conditional from formula A to formula B, followed by formula A; and true position formula B

1 occurrence in this chapter

Equation form expr-7a38e50af092b334

Γ∣Π∣Δ,A∨B\Gamma \nSequent \Pi \nSequent \Delta, !A \lor !B

Read as: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the disjunction of formulas A and B

Means: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the disjunction of formulas A and B

1 occurrence in this chapter

Equation form expr-7c5cce71991cac2a

Γ∣A∧B,Π∣Δ\Gamma \nSequent !A \land !B, \Pi \nSequent \Delta

Read as: the three sided sequent with false position Gamma; middle position the conjunction of formulas A and B, followed by Pi; and true position Delta

Means: the three sided sequent with false position Gamma; middle position the conjunction of formulas A and B, followed by Pi; and true position Delta

1 occurrence in this chapter

Equation form expr-7e8a15c738143b4f

B∣B,A∣BB \nSequent B, A \nSequent B

Read as: the three sided sequent with false position formula B; middle position formula B, followed by formula A; and true position formula B

Means: the three sided sequent with false position formula B; middle position formula B, followed by formula A; and true position formula B

1 occurrence in this chapter

Equation form expr-803b98097bd044e4

→F\iR\lif\False

Read as: conditional rule at position false

Means: conditional rule at position false

1 occurrence in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: A

Means: A

7 occurrences in this chapter

Equation form expr-8405f642bb483576

Γ1∣…∣A,Γi∣…∣Γn\Gamma_1 \nSequent \dots \nSequent \phantom{!A,}\Gamma_i \nSequent \dots \nSequent \Gamma_n

Read as: the n sided sequent containing Gamma sub one through Gamma sub n, with Gamma sub i in position i; the phantom formula is alignment space only

Means: the n sided sequent containing Gamma sub one through Gamma sub n, with Gamma sub i in position i; the phantom formula is alignment space only

1 occurrence in this chapter

Equation form expr-89c03896330cd2b6

→Ł3F\iR\lif\False[\LogLuk[3]]

Read as: conditional rule at position false in three valued Lukasiewicz logic

Means: conditional rule at position false in three valued Lukasiewicz logic

1 occurrence in this chapter

Equation form expr-8a9e0fe61f04fd56

B,B,A∣A∣B,AB, B, A \nSequent A \nSequent B, A

Read as: the three sided sequent with false position formula B, followed by formula B, followed by formula A; middle position formula A; and true position formula B, followed by formula A

Means: the three sided sequent with false position formula B, followed by formula B, followed by formula A; middle position formula A; and true position formula B, followed by formula A

1 occurrence in this chapter

Equation form expr-8cca39d6fd746425

Γ,Δ,Π,Λ\Gamma, \Delta, \Pi, \Lambda

Read as: Gamma, Delta, Pi, and Lambda

Means: Gamma, Delta, Pi, and Lambda

1 occurrence in this chapter

Equation form expr-8dbcf470742605a1

Γ∣B,Π∣Δ\Gamma \nSequent !B, \Pi \nSequent \Delta

Read as: the three sided sequent with false position Gamma; middle position formula B, followed by Pi; and true position Delta

Means: the three sided sequent with false position Gamma; middle position formula B, followed by Pi; and true position Delta

1 occurrence in this chapter

Equation form expr-9173814377bb020a

A,Γ∣A,Π∣Δ!A, \Gamma \nSequent !A, \Pi \nSequent \Delta

Read as: the three sided sequent with false position formula A, followed by Gamma; middle position formula A, followed by Pi; and true position Delta

Means: the three sided sequent with false position formula A, followed by Gamma; middle position formula A, followed by Pi; and true position Delta

1 occurrence in this chapter

Equation form expr-9337c24cc88f985d

v¯(B)=F\pValue v(!B) = \False

Read as: the value of formula B under valuation v is false

Means: the value of formula B under valuation v is false

1 occurrence in this chapter

Equation form expr-9393bdc81a0b2554

B,A∣A∣B,A,AB, A \nSequent A \nSequent B, A, A

Read as: the three sided sequent with false position formula B, followed by formula A; middle position formula A; and true position formula B, followed by formula A, followed by formula A

Means: the three sided sequent with false position formula B, followed by formula A; middle position formula A; and true position formula B, followed by formula A, followed by formula A

1 occurrence in this chapter

Equation form expr-97b525b19e5d6091

A,Γ∣Π∣Δ!A, \Gamma \nSequent \Pi \nSequent \Delta

Read as: the three sided sequent with false position formula A, followed by Gamma; middle position Pi; and true position Delta

Means: the three sided sequent with false position formula A, followed by Gamma; middle position Pi; and true position Delta

3 occurrences in this chapter

Equation form expr-991452eb5f9ffd70

Γ∣Π∣Δ,¬A\Gamma \nSequent \Pi \nSequent \Delta, \lnot !A

Read as: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the negation of formula A

Means: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the negation of formula A

2 occurrences in this chapter

Equation form expr-9b01d5ae7fc3bccc

Γ1∣…∣A,Γi∣…∣Γn\Gamma_1 \nSequent \dots \nSequent !A, \Gamma_i \nSequent \dots \nSequent \Gamma_n

Read as: the n sided sequent containing Gamma sub one through Gamma sub n, except that position i contains formula A followed by Gamma sub i

Means: the n sided sequent containing Gamma sub one through Gamma sub n, except that position i contains formula A followed by Gamma sub i

1 occurrence in this chapter

Equation form expr-9eda799ba8486ea7

v¯(A)=T\pValue v(!A) = \True

Read as: the value of formula A under valuation v is true

Means: the value of formula A under valuation v is true

2 occurrences in this chapter

Equation form expr-a04cd30d75ac8eb8

i≠ji \neq j

Read as: where i differs from j

Means: where i differs from j

1 occurrence in this chapter

Equation form expr-a0cbb5b30ceb8f09

A∈Δ!A \in \Delta

Read as: A in Delta

Means: A in Delta

2 occurrences in this chapter

Equation form expr-a1aeb29e21b0627f

Γ∣Π∣Δ,A→B\Gamma \nSequent \Pi \nSequent \Delta, !A \lif !B

Read as: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the conditional from formula A to formula B

Means: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the conditional from formula A to formula B

3 occurrences in this chapter

Equation form expr-a1ec5eb6d8612789

L\Log{L}

Read as: L

Means: L

7 occurrences in this chapter

Equation form expr-a25d9c9866c45520

Γ0⊆Γ\Gamma_0 \subseteq \Gamma

Read as: Gamma sub zero of Gamma

Means: Gamma sub zero of Gamma

1 occurrence in this chapter

Equation form expr-a37bce9779209494

v¯(A)=T\pValue{v}(!A) = \True

Read as: the value of formula A under valuation v is true

Means: the value of formula A under valuation v is true

2 occurrences in this chapter

Equation form expr-a405ece56ee84cb7

Γ⇒Δ,A,B\Gamma \fCenter \Delta, !A, !B

Read as: the two sided sequent with antecedent Gamma and succedent Delta, followed by formula A, followed by formula B

Means: the two sided sequent with antecedent Gamma and succedent Delta, followed by formula A, followed by formula B

1 occurrence in this chapter

Equation form expr-a4cd101fc0b5f98e

⊢LA\Proves[\Log{L}] !A

Read as: formula A is a theorem of logic L

Means: formula A is a theorem of logic L

1 occurrence in this chapter

Equation form expr-a88fe1192acd5d21

A1,…,An⇒B1,…,Bncan be interpreted as the formula(A1∧⋯∧Am)→(B1∨⋯∨Bn)!A_1, \dots, !A_n & \Sequent !B_1, \dots, !B_n \intertext{can be interpreted as the !!{formula}} (!A_1 \land \cdots \land !A_m) & \lif (!B_1 \lor \cdots \lor !B_n)

Read as: The first row is the sequent with antecedent formulas A sub one through A sub n and succedent formulas B sub one through B sub n. The source says this can be interpreted as the formula whose antecedent is the conjunction of A sub one through A sub m and whose consequent is the disjunction of B sub one through B sub n. The source uses n in the first antecedent list and m in the second; that mismatch is preserved and separately noted.

Means: The first row is the sequent with antecedent formulas A sub one through A sub n and succedent formulas B sub one through B sub n. The source says this can be interpreted as the formula whose antecedent is the conjunction of A sub one through A sub m and whose consequent is the disjunction of B sub one through B sub n. The source uses n in the first antecedent list and m in the second; that mismatch is preserved and separately noted.

1 occurrence in this chapter

Equation form expr-a95252ad3a4e92c8

B∣B∣BB \nSequent B \nSequent B

Read as: the three sided sequent with false position formula B; middle position formula B; and true position formula B

Means: the three sided sequent with false position formula B; middle position formula B; and true position formula B

1 occurrence in this chapter

Equation form expr-aa122470d608ed04

v¯(A)=U\pValue{v}(!A) = \Undef

Read as: the value of formula A under valuation v is the middle truth value

Means: the value of formula A under valuation v is the middle truth value

1 occurrence in this chapter

Equation form expr-ab8c1edb61dc3104

∧U\iR\land\Undef

Read as: conjunction rule at position middle

Means: conjunction rule at position middle

1 occurrence in this chapter

Equation form expr-b066a97bd1545784

A∣A∣B,A,AA \nSequent A \nSequent B, A, A

Read as: the three sided sequent with false position formula A; middle position formula A; and true position formula B, followed by formula A, followed by formula A

Means: the three sided sequent with false position formula A; middle position formula A; and true position formula B, followed by formula A, followed by formula A

1 occurrence in this chapter

Equation form expr-b0d70303c7fd3bf4

∧T\iR\land\True

Read as: conjunction rule at position true

Means: conjunction rule at position true

1 occurrence in this chapter

Equation form expr-b20561e8f21bff07

Γ1∣…∣A,Γi∣…∣ΓnΔ1∣…∣A,Δj∣…∣ΔnΓ1,Δ1∣…∣Γn,ΔnCuti,j\AxiomC{$ \Gamma_1 \nSequent \dots \nSequent !A, \Gamma_i \nSequent \dots \nSequent \Gamma_n $} \AxiomC{$ \Delta_1 \nSequent \dots \nSequent !A, \Delta_j \nSequent \dots \nSequent \Delta_n $} \RightLabel{$\iR{\Cut}{i,j}$} \BinaryInfC{$\Gamma_1,\Delta_1 \nSequent \dots \nSequent \Gamma_n, \Delta_n$} \DisplayProof

Read as: Cut rule at distinct positions i and j. The first premise is the n sided sequent with formula A followed by Gamma sub i in position i and Gamma sub k in every other position k. The second premise has formula A followed by Delta sub j in position j and Delta sub k in every other position k. From both premises, in this order, infer the n sided sequent whose position k contains Gamma sub k followed by Delta sub k. Formula A is removed from the two distinguished positions. End cut rule.

Means: Cut rule at distinct positions i and j. The first premise is the n sided sequent with formula A followed by Gamma sub i in position i and Gamma sub k in every other position k. The second premise has formula A followed by Delta sub j in position j and Delta sub k in every other position k. From both premises, in this order, infer the n sided sequent whose position k contains Gamma sub k followed by Delta sub k. Formula A is removed from the two distinguished positions. End cut rule.

1 occurrence in this chapter

Equation form expr-b4c71fc401032f6a

A,Γ∣Π∣Δ,B!A, \Gamma \nSequent \Pi \nSequent \Delta, !B

Read as: the three sided sequent with false position formula A, followed by Gamma; middle position Pi; and true position Delta, followed by formula B

Means: the three sided sequent with false position formula A, followed by Gamma; middle position Pi; and true position Delta, followed by formula B

1 occurrence in this chapter

Equation form expr-b9ad434e01722a0d

B∣A,B∣BB \nSequent A, B \nSequent B

Read as: the three sided sequent with false position formula B; middle position formula A, followed by formula B; and true position formula B

Means: the three sided sequent with false position formula B; middle position formula A, followed by formula B; and true position formula B

1 occurrence in this chapter

Equation form expr-bb8224d2fb111ef9

A⇒A!A \Sequent !A

Read as: with A in both the antecedent and the succedent

Means: with A in both the antecedent and the succedent

1 occurrence in this chapter

Equation form expr-bc9367794d2761fe

A∈Γ!A \in \Gamma

Read as: A in Gamma

Means: A in Gamma

2 occurrences in this chapter

Equation form expr-bca44b958c91efd8

A,B,Γ∣Π∣Δ!A, !B, \Gamma \nSequent \Pi \nSequent \Delta

Read as: the three sided sequent with false position formula A, followed by formula B, followed by Gamma; middle position Pi; and true position Delta

Means: the three sided sequent with false position formula A, followed by formula B, followed by Gamma; middle position Pi; and true position Delta

1 occurrence in this chapter

Equation form expr-bdcb7192fe841cb0

v\pAssign v

Read as: v

Means: v

1 occurrence in this chapter

Equation form expr-be2fa09c77ad3a0a

→U\iR\lif\Undef

Read as: conditional rule at position middle

Means: conditional rule at position middle

2 occurrences in this chapter

Equation form expr-bf54238606d42e91

v¯(A→B)=T\pValue v(!A \lif !B) = \True

Read as: the value of the conditional from A to B under valuation v is true

Means: the value of the conditional from A to B under valuation v is true

1 occurrence in this chapter

Equation form expr-c4d44cc35a34661e

B,Γ∣Π∣Δ!B, \Gamma \nSequent \Pi \nSequent \Delta

Read as: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta

Means: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta

4 occurrences in this chapter

Equation form expr-c63f9557f464c93a

¬A\lnot !A

Read as: the negation of formula A

Means: the negation of formula A

1 occurrence in this chapter

Equation form expr-c6f2859802be1886

→KsF\iR\lif\False[\LogKs]

Read as: conditional rule at position false in strong Kleene logic

Means: conditional rule at position false in strong Kleene logic

1 occurrence in this chapter

Equation form expr-c89fabbd98da1d36

Γ∣A,Π∣A,Δ\Gamma \nSequent !A, \Pi \nSequent !A, \Delta

Read as: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position formula A, followed by Delta

Means: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position formula A, followed by Delta

1 occurrence in this chapter

Equation form expr-ca474ab430f140ef

v¯(A)=F\pValue v(!A) = \False

Read as: the value of formula A under valuation v is false

Means: the value of formula A under valuation v is false

1 occurrence in this chapter

Equation form expr-cf7c3530e6822cc5

A∧B,Γ⇒Δ!A \land !B, \Gamma \fCenter \Delta

Read as: the two sided sequent with antecedent the conjunction of formulas A and B, followed by Gamma and succedent Delta

Means: the two sided sequent with antecedent the conjunction of formulas A and B, followed by Gamma and succedent Delta

1 occurrence in this chapter

Equation form expr-d03543adcda36df1

Γ0\Gamma_0

Read as: Gamma sub zero

Means: Gamma sub zero

1 occurrence in this chapter

Equation form expr-d04ff80d9f6dc462

→\lif

Read as: the conditional connective

Means: the conditional connective

4 occurrences in this chapter

Equation form expr-d160169ee7c069c0

∨T\iR\lor\True

Read as: disjunction rule at position true

Means: disjunction rule at position true

1 occurrence in this chapter

Equation form expr-d1ece4de0c21edf2

B,Γ∣B,Π∣Δ!B, \Gamma \nSequent !B, \Pi \nSequent \Delta

Read as: the three sided sequent with false position formula B, followed by Gamma; middle position formula B, followed by Pi; and true position Delta

Means: the three sided sequent with false position formula B, followed by Gamma; middle position formula B, followed by Pi; and true position Delta

2 occurrences in this chapter

Equation form expr-d36f44d342af84d0

∨R\RightR{\lor}

Read as: right disjunction

Means: right disjunction

1 occurrence in this chapter

Equation form expr-d3701e0b5a1a9160

Γ∣A,Π∣Δ,A\Gamma \nSequent !A, \Pi \nSequent \Delta, !A

Read as: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula A

Means: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula A

3 occurrences in this chapter

Equation form expr-d73a1e5bfac0197f

⊬LA\Proves/[\Log{L}] !A

Read as: formula A is not a theorem of logic L

Means: formula A is not a theorem of logic L

1 occurrence in this chapter

Equation form expr-d798ad41124aaebf

A→B⇒!A \lif !B \fCenter

Read as: the two sided sequent with antecedent the conditional from formula A to formula B and succedent empty

Means: the two sided sequent with antecedent the conditional from formula A to formula B and succedent empty

1 occurrence in this chapter

Equation form expr-da7ba73a9a4fe474

¬A,Γ∣Π∣Δ\lnot !A, \Gamma \nSequent \Pi \nSequent \Delta

Read as: the three sided sequent with false position the negation of formula A, followed by Gamma; middle position Pi; and true position Delta

Means: the three sided sequent with false position the negation of formula A, followed by Gamma; middle position Pi; and true position Delta

2 occurrences in this chapter

Equation form expr-dafaf5a8520aea16

→Ł3U\iR\lif\Undef[\LogLuk[3]]

Read as: conditional rule at position middle in three valued Lukasiewicz logic

Means: conditional rule at position middle in three valued Lukasiewicz logic

1 occurrence in this chapter

Equation form expr-db80c2791e4d871e

Γ∣A→B,Π∣Δ\Gamma \nSequent !A \lif !B, \Pi \nSequent \Delta

Read as: the three sided sequent with false position Gamma; middle position the conditional from formula A to formula B, followed by Pi; and true position Delta

Means: the three sided sequent with false position Gamma; middle position the conditional from formula A to formula B, followed by Pi; and true position Delta

3 occurrences in this chapter

Equation form expr-dd89bb82912fdfa4

→Ł3T\iR{\lif}{\True}[\LogLuk[3]]

Read as: conditional rule at position true in three valued Lukasiewicz logic

Means: conditional rule at position true in three valued Lukasiewicz logic

1 occurrence in this chapter

Equation form expr-de5a6f78116eca62

VV

Read as: the set V of truth values

Means: the set V of truth values

1 occurrence in this chapter

Equation form expr-de7d1b721a1e0632

ii

Read as: i

Means: i

2 occurrences in this chapter

Equation form expr-de93224b3b30e3e2

Γ⇒Δ\Gamma \Sequent \Delta

Read as: with antecedent Gamma and succedent Delta

Means: with antecedent Gamma and succedent Delta

1 occurrence in this chapter

Equation form expr-e03c7dabfdcd4879

Γ∣Π∣Δ\Gamma \nSequent \Pi \nSequent \Delta

Read as: with Gamma in the false position, Pi in the middle position, and Delta in the true position

Means: with Gamma in the false position, Pi in the middle position, and Delta in the true position

1 occurrence in this chapter

Equation form expr-e32441dded7d5cf8

Γ1∣…∣A,A,Γi∣…∣Γn\Gamma_1 \nSequent \dots \nSequent \phantom{!A,}!A, \Gamma_i \nSequent \dots \nSequent \Gamma_n

Read as: the n sided sequent containing Gamma sub one through Gamma sub n, except that position i contains one visible copy of formula A followed by Gamma sub i; the phantom copy is alignment space only

Means: the n sided sequent containing Gamma sub one through Gamma sub n, except that position i contains one visible copy of formula A followed by Gamma sub i; the phantom copy is alignment space only

1 occurrence in this chapter

Equation form expr-e44509fb8b6d046d

Γ∣A∨B,Π∣Δ\Gamma \nSequent !A \lor !B, \Pi \nSequent \Delta

Read as: the three sided sequent with false position Gamma; middle position the disjunction of formulas A and B, followed by Pi; and true position Delta

Means: the three sided sequent with false position Gamma; middle position the disjunction of formulas A and B, followed by Pi; and true position Delta

1 occurrence in this chapter

Equation form expr-e446c94f13610096

Γ1∣…∣A,A,Γi∣…∣Γn\Gamma_1 \nSequent \dots \nSequent !A, !A, \Gamma_i \nSequent \dots \nSequent \Gamma_n

Read as: the n sided sequent containing Gamma sub one through Gamma sub n, except that position i contains two consecutive copies of formula A followed by Gamma sub i

Means: the n sided sequent containing Gamma sub one through Gamma sub n, except that position i contains two consecutive copies of formula A followed by Gamma sub i

1 occurrence in this chapter

Equation form expr-e77ee8d5c40541a6

Γ1∣…∣Γi,A,B,Γi′∣…∣Γn\Gamma_1 \nSequent \dots \nSequent \Gamma_i, !A, !B, \Gamma_i' \nSequent \dots \nSequent \Gamma_n

Read as: the n sided sequent with position i containing Gamma sub i, formula A, formula B, then Gamma sub i prime; all other positions retain their respective Gamma sequences

Means: the n sided sequent with position i containing Gamma sub i, formula A, formula B, then Gamma sub i prime; all other positions retain their respective Gamma sequences

1 occurrence in this chapter

Equation form expr-eb3c7ecd0e83e652

Wi\iR{\Weakening}{i}

Read as: weakening rule at position i

Means: weakening rule at position i

1 occurrence in this chapter

Equation form expr-eb5e9ce47e79ae0b

Γ∣Π∣Δ,A∧B\Gamma \nSequent \Pi \nSequent \Delta, !A \land !B

Read as: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the conjunction of formulas A and B

Means: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the conjunction of formulas A and B

1 occurrence in this chapter

Equation form expr-ec165f474a12cdd8

A∈Π!A \in \Pi

Read as: A in Pi

Means: A in Pi

1 occurrence in this chapter

Equation form expr-efa51acdf0e7c3c4

L\Lang L

Read as: L

Means: L

1 occurrence in this chapter

Equation form expr-f1941b975ffcc891

Δ\Delta

Read as: Delta

Means: Delta

2 occurrences in this chapter

Equation form expr-f1b1ee0e16fb553d

A∣A∣A!A \mid !A \mid !A

Read as: with A in each of the false, middle, and true positions

Means: with A in each of the false, middle, and true positions

1 occurrence in this chapter

Equation form expr-f33969fcce38a6f4

Λ1∣…∣Λn\Lambda_1 \nSequent \dots \nSequent \Lambda_n

Read as: the n sided sequent whose positions, in order, contain Lambda sub one through Lambda sub n

Means: the n sided sequent whose positions, in order, contain Lambda sub one through Lambda sub n

1 occurrence in this chapter

Equation form expr-f601774e071f07c0

B,A∣A∣B,AB, A \nSequent A \nSequent B, A

Read as: the three sided sequent with false position formula B, followed by formula A; middle position formula A; and true position formula B, followed by formula A

Means: the three sided sequent with false position formula B, followed by formula A; middle position formula A; and true position formula B, followed by formula A

1 occurrence in this chapter

Equation form expr-f6ac033cc1d1554a

Γ⊬A\Gamma \Proves/ !A

Read as: formula A is not derivable from Gamma

Means: formula A is not derivable from Gamma

1 occurrence in this chapter

Equation form expr-f9a3f5719f4b3a2b

Xi\iR{\Exchange}{i}

Read as: exchange rule at position i

Means: exchange rule at position i

1 occurrence in this chapter

Equation form expr-f9ab5b7aa897477c

…∣⋆∣…\dots \nSequent \star \nSequent \dots

Read as: with star in one position

Means: with star in one position

1 occurrence in this chapter

Equation form expr-f9baaf9f77711629

F\False

Read as: the false truth value

Means: the false truth value

1 occurrence in this chapter

Equation form expr-fa2f55ffb56cc927

⋆~∈V\tf{\star} \in V

Read as: the truth value assigned by the nullary truth function for star, which belongs to V

Means: the truth value assigned by the nullary truth function for star, which belongs to V

1 occurrence in this chapter

Equation form expr-fd529810b398040b

B,Γ∣Π∣Δ,A!B, \Gamma \nSequent \Pi \nSequent \Delta, !A

Read as: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta, followed by formula A

Means: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta, followed by formula A

1 occurrence in this chapter

Classical sequent interpretation

The display relates a classical sequent to a conditional with a conjunction as antecedent and a disjunction as consequent. The source switches from n to m for the end of the antecedent list. Both original rows and the mismatch are preserved; no silently repaired equivalence is asserted.

Source

Classical conditional rules

The left conditional rule has two ordered premises, empty antecedent with A as succedent, then B as antecedent with empty succedent. Its conclusion has the conditional from A to B as antecedent and empty succedent. The right conditional rule has one premise, A as antecedent and B as succedent, and concludes with empty antecedent and that conditional as succedent. Side formulas are omitted as stated in the source.

Source

Classical left conditional rule

Proof tree. Classical left conditional rule. Premise node one: the two sided sequent with antecedent empty and succedent formula A. Premise node two: the two sided sequent with antecedent formula B and succedent empty. The label of the next inference is left conditional rule. From nodes one, and two, in that order, infer node three: the two sided sequent with antecedent the conditional from formula A to formula B and succedent empty. The root conclusion is node three. End proof tree.

Source

Classical right conditional rule

Proof tree. Classical right conditional rule. Premise node one: the two sided sequent with antecedent formula A and succedent formula B. The label of the next inference is right conditional rule. From node one, in that order, infer node two: the two sided sequent with antecedent empty and succedent the conditional from formula A to formula B. The root conclusion is node two. End proof tree.

Source

Alternative classical conjunction and disjunction rules

The left conjunction version replaces adjacent formulas A and B in the antecedent by their conjunction. The right disjunction version replaces adjacent formulas A and B in the succedent by their disjunction. Each has one premise, and all Gamma and Delta side sequences retain their positions.

Source

Alternative classical left conjunction rule

Proof tree. Alternative classical left conjunction rule. Premise node one: the two sided sequent with antecedent formula A, followed by formula B, followed by Gamma and succedent Delta. The label of the next inference is left conjunction rule. From node one, in that order, infer node two: the two sided sequent with antecedent the conjunction of formulas A and B, followed by Gamma and succedent Delta. The root conclusion is node two. End proof tree.

Source

Alternative classical right disjunction rule

Proof tree. Alternative classical right disjunction rule. Premise node one: the two sided sequent with antecedent Gamma and succedent Delta, followed by formula A, followed by formula B. The label of the next inference is right disjunction rule. From node one, in that order, infer node two: the two sided sequent with antecedent Gamma and succedent Delta, followed by the disjunction of formulas A and B. The root conclusion is node two. End proof tree.

Source

Definition of an n sided sequent

An n sided sequent has one finite, possibly empty sequence of sentences in each of its n positions. The displayed list runs from Gamma sub one through Gamma sub n. The following prose erroneously repeats Gamma sub one and uses the plural sequences after a singular subject; those source defects are preserved with a note.

Source

Definition of initial sequents

One initial sequent contains the same sentence A in every position. A nullary connective also supplies an initial sequent with that propositional constant in its associated truth value position, all other positions empty. These are two source-specified forms, not extra derivations supplied by the edition.

Source

Definition of theoremhood

A sentence is a theorem when a derivation concludes with that sentence in every position corresponding to a designated truth value. The positive and negative provability notations are distinguished. A non-designated position is not filled with an invented formula.

Source

Definition of derivability from premises

Choose a finite subset of Gamma and an ordered sequence of its sentences. In each designated position put the conclusion sentence A; in each other position put that chosen premise sequence. A derivation of the resulting n sided sequent establishes derivability. The finite set Gamma sub zero and its sequence Gamma sub zero prime have different roles. The final notation denotes failure of derivability.

Source

Indexed structural rules

Weakening inserts a sentence at position i. Contraction replaces two adjacent occurrences by one. Exchange reverses the order of two adjacent sentences between the unchanged context sequences at position i. Every other position is unchanged. Phantom text in the displayed schemata is invisible alignment material and is not an extra premise formula.

Source

Weakening at an arbitrary position

Proof tree. Weakening at an arbitrary position. Premise node one: the n sided sequent containing Gamma sub one through Gamma sub n, with Gamma sub i in position i; the phantom formula is alignment space only. The label of the next inference is weakening rule at position i. From node one, in that order, infer node two: the n sided sequent containing Gamma sub one through Gamma sub n, except that position i contains formula A followed by Gamma sub i. The root conclusion is node two. End proof tree.

Source

Contraction at an arbitrary position

Proof tree. Contraction at an arbitrary position. Premise node one: the n sided sequent containing Gamma sub one through Gamma sub n, except that position i contains two consecutive copies of formula A followed by Gamma sub i. The label of the next inference is contraction rule at position i. From node one, in that order, infer node two: the n sided sequent containing Gamma sub one through Gamma sub n, except that position i contains one visible copy of formula A followed by Gamma sub i; the phantom copy is alignment space only. The root conclusion is node two. End proof tree.

Source

Exchange at an arbitrary position

Proof tree. Exchange at an arbitrary position. Premise node one: the n sided sequent with position i containing Gamma sub i, formula A, formula B, then Gamma sub i prime; all other positions retain their respective Gamma sequences. The label of the next inference is exchange rule at position i. From node one, in that order, infer node two: the n sided sequent with position i containing Gamma sub i, formula B, formula A, then Gamma sub i prime; all other positions retain their respective Gamma sequences. The root conclusion is node two. End proof tree.

Source

Cut at distinct positions

Cut uses two premises in which A occupies different truth value positions i and j. The conclusion concatenates the respective Gamma and Delta context sequences at each position and removes the two displayed distinguished occurrences of A. The source explicitly requires i and j to differ. The whole proof is one frozen outer display occurrence; its internal node topology is retained separately.

Source

Cut at two distinct positions

Cut rule at distinct positions i and j. The first premise is the n sided sequent with formula A followed by Gamma sub i in position i and Gamma sub k in every other position k. The second premise has formula A followed by Delta sub j in position j and Delta sub k in every other position k. From both premises, in this order, infer the n sided sequent whose position k contains Gamma sub k followed by Delta sub k. Formula A is removed from the two distinguished positions. End cut rule.

Source

Negation for Lukasiewicz and Kleene logics

The three rules move A from true to the negation of A at false, keep a middle valued A as its negation at middle, or move a false A to its negation at true. Each rule has one premise and preserves all side contexts.

Source

False position negation rule for Lukasiewicz and Kleene logics

Proof tree. False position negation rule for Lukasiewicz and Kleene logics. Premise node one: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A. The label of the next inference is negation rule at position false. From node one, in that order, infer node two: the three sided sequent with false position the negation of formula A, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node two. End proof tree.

Source

Middle position negation rule for Lukasiewicz and Kleene logics

Proof tree. Middle position negation rule for Lukasiewicz and Kleene logics. Premise node one: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position Delta. The label of the next inference is negation rule at position middle. From node one, in that order, infer node two: the three sided sequent with false position Gamma; middle position the negation of formula A, followed by Pi; and true position Delta. The root conclusion is node two. End proof tree.

Source

True position negation rule for Lukasiewicz and Kleene logics

Proof tree. True position negation rule for Lukasiewicz and Kleene logics. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is negation rule at position true. From node one, in that order, infer node two: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the negation of formula A. The root conclusion is node two. End proof tree.

Source

Negation for Goedel logic

The false negation rule has one premise placing A in both middle and true positions; satisfaction of that premise permits either value. Its conclusion places not A in the false position. The true negation rule moves A from false to not A at true. No middle negation rule is given, because Goedel negation never has the middle value.

Source

False position negation rule for Goedel logic

Proof tree. False position negation rule for Goedel logic. Premise node one: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula A. The label of the next inference is negation rule at position false in Goedel logic. From node one, in that order, infer node two: the three sided sequent with false position the negation of formula A, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node two. End proof tree.

Source

True position negation rule for Goedel logic

Proof tree. True position negation rule for Goedel logic. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is negation rule at position true in Goedel logic. From node one, in that order, infer node two: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the negation of formula A. The root conclusion is node two. End proof tree.

Source

Conjunction rules for the three selected logics

For false conjunction there is one premise with both conjuncts on the false side. For middle conjunction there are three premises: A in middle or true, B in middle or true, and at least one conjunct in middle. For true conjunction there are two premises, one requiring A true and one requiring B true. Side formulas remain as printed. The premises of a multi-premise inference are jointly required, not alternatives.

Source

False position conjunction rule

Proof tree. False position conjunction rule. Premise node one: the three sided sequent with false position formula A, followed by formula B, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is conjunction rule at position false. From node one, in that order, infer node two: the three sided sequent with false position the conjunction of formulas A and B, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node two. End proof tree.

Source

Middle position conjunction rule

Proof tree. Middle position conjunction rule. Premise node one: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position formula A, followed by Delta. Premise node two: the three sided sequent with false position Gamma; middle position formula B, followed by Pi; and true position formula B, followed by Delta. Premise node three: the three sided sequent with false position Gamma; middle position formula A, followed by formula B, followed by Pi; and true position Delta. The label of the next inference is conjunction rule at position middle. From nodes one, and two, and three, in that order, infer node four: the three sided sequent with false position Gamma; middle position the conjunction of formulas A and B, followed by Pi; and true position Delta. The root conclusion is node four. End proof tree.

Source

True position conjunction rule

Proof tree. True position conjunction rule. Premise node one: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A. Premise node two: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula B. The label of the next inference is conjunction rule at position true. From nodes one, and two, in that order, infer node three: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the conjunction of formulas A and B. The root conclusion is node three. End proof tree.

Source

Disjunction rules for the three selected logics

For false disjunction both A false and B false premises are required. For middle disjunction three premises require each disjunct to be false or middle and at least one to be middle. For true disjunction a single premise permits either disjunct on the true side. Formula order and multiplicity are preserved.

Source

False position disjunction rule

Proof tree. False position disjunction rule. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position Pi; and true position Delta. Premise node two: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is disjunction rule at position false. From nodes one, and two, in that order, infer node three: the three sided sequent with false position the disjunction of formulas A and B, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node three. End proof tree.

Source

Middle position disjunction rule

Proof tree. Middle position disjunction rule. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position formula A, followed by Pi; and true position Delta. Premise node two: the three sided sequent with false position formula B, followed by Gamma; middle position formula B, followed by Pi; and true position Delta. Premise node three: the three sided sequent with false position Gamma; middle position formula A, followed by formula B, followed by Pi; and true position Delta. The label of the next inference is disjunction rule at position middle. From nodes one, and two, and three, in that order, infer node four: the three sided sequent with false position Gamma; middle position the disjunction of formulas A and B, followed by Pi; and true position Delta. The root conclusion is node four. End proof tree.

Source

True position disjunction rule

Proof tree. True position disjunction rule. Premise node one: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A, followed by formula B. The label of the next inference is disjunction rule at position true. From node one, in that order, infer node two: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the disjunction of formulas A and B. The root conclusion is node two. End proof tree.

Source

Conditional rules for three valued Lukasiewicz logic

False, middle, and true conditional rules each have two ordered premises. Within any one sequent the displayed positions are interpreted disjunctively; distinct premises of an inference must all be satisfied. The proof templates retain the exact occurrences of A and B in each position and the Lukasiewicz rule labels.

Source

False position conditional rule for three valued Lukasiewicz logic

Proof tree. False position conditional rule for three valued Lukasiewicz logic. Premise node one: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A. Premise node two: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is conditional rule at position false in three valued Lukasiewicz logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position the conditional from formula A to formula B, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node three. End proof tree.

Source

Middle position conditional rule for three valued Lukasiewicz logic

Proof tree. Middle position conditional rule for three valued Lukasiewicz logic. Premise node one: the three sided sequent with false position Gamma; middle position formula A, followed by formula B, followed by Pi; and true position Delta. Premise node two: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta, followed by formula A. The label of the next inference is conditional rule at position middle in three valued Lukasiewicz logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position Gamma; middle position the conditional from formula A to formula B, followed by Pi; and true position Delta. The root conclusion is node three. End proof tree.

Source

True position conditional rule for three valued Lukasiewicz logic

Proof tree. True position conditional rule for three valued Lukasiewicz logic. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position formula B, followed by Pi; and true position Delta, followed by formula B. Premise node two: the three sided sequent with false position formula A, followed by Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula B. The label of the next inference is conditional rule at position true in three valued Lukasiewicz logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the conditional from formula A to formula B. The root conclusion is node three. End proof tree.

Source

Conditional rules for strong Kleene logic

The false conditional rule has two premises, the middle conditional rule three, and the true conditional rule one. Their position patterns encode the corresponding strong Kleene truth conditions. A formula repeated across positions represents a disjunction of value possibilities within that sequent, not several separate required truth values.

Source

False position conditional rule for strong Kleene logic

Proof tree. False position conditional rule for strong Kleene logic. Premise node one: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A. Premise node two: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is conditional rule at position false in strong Kleene logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position the conditional from formula A to formula B, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node three. End proof tree.

Source

Middle position conditional rule for strong Kleene logic

Proof tree. Middle position conditional rule for strong Kleene logic. Premise node one: the three sided sequent with false position formula B, followed by Gamma; middle position formula B, followed by Pi; and true position Delta. Premise node two: the three sided sequent with false position Gamma; middle position formula A, followed by formula B, followed by Pi; and true position Delta. Premise node three: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula A. The label of the next inference is conditional rule at position middle in strong Kleene logic. From nodes one, and two, and three, in that order, infer node four: the three sided sequent with false position Gamma; middle position the conditional from formula A to formula B, followed by Pi; and true position Delta. The root conclusion is node four. End proof tree.

Source

True position conditional rule for strong Kleene logic

Proof tree. True position conditional rule for strong Kleene logic. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position Pi; and true position Delta, followed by formula B. The label of the next inference is conditional rule at position true in strong Kleene logic. From node one, in that order, infer node two: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the conditional from formula A to formula B. The root conclusion is node two. End proof tree.

Source

Conditional rules for three valued Goedel logic

The false, middle, and true conditional rules each have two premises. The false rule allows A in the middle or true position while B is false. The middle rule requires B middle and A true. The true rule uses the two displayed disjunctive premises, preserving all repetitions and side contexts.

Source

False position conditional rule for three valued Goedel logic

Proof tree. False position conditional rule for three valued Goedel logic. Premise node one: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula A. Premise node two: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is conditional rule at position false in three valued Goedel logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position the conditional from formula A to formula B, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node three. End proof tree.

Source

Middle position conditional rule for three valued Goedel logic

Proof tree. Middle position conditional rule for three valued Goedel logic. Premise node one: the three sided sequent with false position Gamma; middle position formula B, followed by Pi; and true position Delta. Premise node two: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A. The label of the next inference is conditional rule at position middle in three valued Goedel logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position Gamma; middle position the conditional from formula A to formula B, followed by Pi; and true position Delta. The root conclusion is node three. End proof tree.

Source

True position conditional rule for three valued Goedel logic

Proof tree. True position conditional rule for three valued Goedel logic. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position formula B, followed by Pi; and true position Delta, followed by formula B. Premise node two: the three sided sequent with false position formula A, followed by Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula B. The label of the next inference is conditional rule at position true in three valued Goedel logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the conditional from formula A to formula B. The root conclusion is node three. End proof tree.

Source

Worked Lukasiewicz derivation figure

The figure is a source-provided branched derivation, not a solution added by this edition. Four initial-sequent leaves are combined through weakening and exchange, two middle conditional inferences, and a final false conditional inference. The final sequent has the conditional from A to B followed by A at both false and middle positions, and B at true. The accompanying proof structure records every branch, rule label, repeated formula and final conclusion; the sideways print orientation has no semantic force.

Source

Worked branched derivation in three valued Lukasiewicz logic

Proof tree. Worked branched derivation in three valued Lukasiewicz logic. Initial sequent node one: the three sided sequent with false position formula A; middle position formula A; and true position formula A. The label of the next inference is weakening rule at position true. From node one, in that order, infer node two: the three sided sequent with false position formula A; middle position formula A; and true position formula B, followed by formula A. The label of the next inference is weakening rule at position middle. From node two, in that order, infer node three: the three sided sequent with false position formula A; middle position formula B, followed by formula A; and true position formula B, followed by formula A. The label of the next inference is weakening rule at position middle. From node three, in that order, infer node four: the three sided sequent with false position formula A; middle position formula A, followed by formula B, followed by formula A; and true position formula B, followed by formula A. Initial sequent node five: the three sided sequent with false position formula A; middle position formula A; and true position formula A. The label of the next inference is weakening rule at position true. From node five, in that order, infer node six: the three sided sequent with false position formula A; middle position formula A; and true position formula A, followed by formula A. The label of the next inference is weakening rule at position true. From node six, in that order, infer node seven: the three sided sequent with false position formula A; middle position formula A; and true position formula B, followed by formula A, followed by formula A. The label of the next inference is weakening rule at position false. From node seven, in that order, infer node eight: the three sided sequent with false position formula B, followed by formula A; middle position formula A; and true position formula B, followed by formula A, followed by formula A. The label of the next inference is conditional rule at position middle. From nodes four, and eight, in that order, infer node nine: the three sided sequent with false position formula A; middle position the conditional from formula A to formula B, followed by formula A; and true position formula B, followed by formula A. Initial sequent node ten: the three sided sequent with false position formula B; middle position formula B; and true position formula B. The label of the next inference is weakening rule at position middle. From node ten, in that order, infer node eleven: the three sided sequent with false position formula B; middle position formula A, followed by formula B; and true position formula B. The label of the next inference is exchange rule at position middle. From node eleven, in that order, infer node twelve: the three sided sequent with false position formula B; middle position formula B, followed by formula A; and true position formula B. The label of the next inference is weakening rule at position middle. From node twelve, in that order, infer node thirteen: the three sided sequent with false position formula B; middle position formula A, followed by formula B, followed by formula A; and true position formula B. The label of the next inference is weakening rule at position false. From node thirteen, in that order, infer node fourteen: the three sided sequent with false position formula A, followed by formula B; middle position formula A, followed by formula B, followed by formula A; and true position formula B. The label of the next inference is exchange rule at position false. From node fourteen, in that order, infer node fifteen: the three sided sequent with false position formula B, followed by formula A; middle position formula A, followed by formula B, followed by formula A; and true position formula B. Initial sequent node sixteen: the three sided sequent with false position formula A; middle position formula A; and true position formula A. The label of the next inference is weakening rule at position true. From node sixteen, in that order, infer node seventeen: the three sided sequent with false position formula A; middle position formula A; and true position formula B, followed by formula A. The label of the next inference is weakening rule at position false. From node seventeen, in that order, infer node eighteen: the three sided sequent with false position formula B, followed by formula A; middle position formula A; and true position formula B, followed by formula A. The label of the next inference is weakening rule at position false. From node eighteen, in that order, infer node nineteen: the three sided sequent with false position formula B, followed by formula B, followed by formula A; middle position formula A; and true position formula B, followed by formula A. The label of the next inference is conditional rule at position middle. From nodes fifteen, and nineteen, in that order, infer node twenty: the three sided sequent with false position formula B, followed by formula A; middle position the conditional from formula A to formula B, followed by formula A; and true position formula B. The label of the next inference is conditional rule at position false. From nodes nine, and twenty, in that order, infer node twenty one: the three sided sequent with false position the conditional from formula A to formula B, followed by formula A; middle position the conditional from formula A to formula B, followed by formula A; and true position formula B. The root conclusion is node twenty one. End proof tree.

Source

Source disclosures

Source-generated mathematical component tr049-source-macro-0001

→L\LeftR{\lif}

Read as: left conditional rule

Read in context source

Source-generated mathematical component tr049-source-macro-0002

→R\RightR{\lif}

Read as: right conditional rule

Read in context source

Source-generated mathematical component tr049-source-macro-0003

∧L\LeftR{\land}

Read as: left conjunction rule

Read in context source

Source-generated mathematical component tr049-source-macro-0004

∨R\RightR{\lor}

Read as: right disjunction rule

Read in context source

Source-generated mathematical component tr049-source-macro-0005

¬F\iR{\lnot}{\False}

Read as: negation rule at position false

Read in context source

Source-generated mathematical component tr049-source-macro-0006

¬U\iR{\lnot}{\Undef}

Read as: negation rule at position middle

Read in context source

Source-generated mathematical component tr049-source-macro-0007

¬T\iR{\lnot}{\True}

Read as: negation rule at position true

Read in context source

Source-generated mathematical component tr049-source-macro-0008

¬GF\iR{\lnot}{\False}[\LogGod]

Read as: negation rule at position false in Goedel logic

Read in context source

Source-generated mathematical component tr049-source-macro-0009

¬GT\iR{\lnot}{\True}[\LogGod]

Read as: negation rule at position true in Goedel logic

Read in context source

Source-generated mathematical component tr049-source-macro-0010

WT\iR \Weakening \True

Read as: weakening rule at position true

Read in context source

Source-generated mathematical component tr049-source-macro-0011

WU\iR \Weakening \Undef

Read as: weakening rule at position middle

Read in context source

Source-generated mathematical component tr049-source-macro-0012

WU\iR \Weakening \Undef

Read as: weakening rule at position middle

Read in context source

Source-generated mathematical component tr049-source-macro-0013

WT\iR \Weakening \True

Read as: weakening rule at position true

Read in context source

Source-generated mathematical component tr049-source-macro-0014

WT\iR \Weakening \True

Read as: weakening rule at position true

Read in context source

Source-generated mathematical component tr049-source-macro-0015

WF\iR \Weakening \False

Read as: weakening rule at position false

Read in context source

Source-generated mathematical component tr049-source-macro-0016

WU\iR \Weakening \Undef

Read as: weakening rule at position middle

Read in context source

Source-generated mathematical component tr049-source-macro-0017

XU\iR \Exchange \Undef

Read as: exchange rule at position middle

Read in context source

Source-generated mathematical component tr049-source-macro-0018

WU\iR \Weakening \Undef

Read as: weakening rule at position middle

Read in context source

Source-generated mathematical component tr049-source-macro-0019

WF\iR \Weakening \False

Read as: weakening rule at position false

Read in context source

Source-generated mathematical component tr049-source-macro-0020

XF\iR \Exchange \False

Read as: exchange rule at position false

Read in context source

Source-generated mathematical component tr049-source-macro-0021

WT\iR \Weakening \True

Read as: weakening rule at position true

Read in context source

Source-generated mathematical component tr049-source-macro-0022

WF\iR \Weakening \False

Read as: weakening rule at position false

Read in context source

Source-generated mathematical component tr049-source-macro-0023

WF\iR \Weakening \False

Read as: weakening rule at position false

Read in context source