The Open Logic Text — accessible offline edition
Natural Deduction
These are conventional contextual readings, not claims that mathematical notation has only one possible pronunciation.
Read as: assumption A, labeled n for discharge
Means: An occurrence of assumption A marked with discharge label n; an inference bearing n may discharge it.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: conjunction
Means: The binary logical connective and, used to form a conjunction.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: disjunction
Means: The binary logical connective or, used to form a disjunction.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: conditional
Means: The binary conditional connective, read as if the antecedent then the consequent.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: negation
Means: The unary logical connective not, used to form a negation.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: a contradiction
Means: The falsum symbol, meaning contradiction.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: formula A
Means: The metavariable A denotes an arbitrary formula.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: formula B
Means: The metavariable B denotes an arbitrary formula.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: A and B
Means: The conjunction of formulas A and B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: A or B
Means: The disjunction of formulas A and B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: formula C
Means: The metavariable C denotes an arbitrary formula.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: assumption B, labeled n for discharge
Means: An occurrence of assumption B marked with discharge label n; an inference bearing n may discharge it.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: if A, then B
Means: The conditional whose antecedent is A and whose consequent is B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: not A
Means: The negation of formula A.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: assumption not A, labeled n for discharge
Means: An occurrence of the negated assumption not A marked with discharge label n.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: negation introduction rule
Means: The natural-deduction rule that infers not A after a contradiction has been derived under assumption A, permitting that assumption to be discharged.
Why this reading: The Open Logic macro expands to the printed name of an inference rule; the result is a rule label, not a formula using that connective.
Read as: classical absurdity rule
Means: The classical natural-deduction rule that infers A from a contradiction derived under assumption not A, permitting that assumption to be discharged.
Why this reading: The subscript C names the classical absurdity rule; it is not formula C and not an index on falsum.
Read as: conditional introduction rule
Means: The natural-deduction rule that infers if A then B from a derivation of B under assumption A, permitting that assumption to be discharged.
Why this reading: The Open Logic macro expands to the printed name of an inference rule; the result is a rule label, not a formula using that connective.
Read as: Gamma
Means: Gamma is the set of undischarged assumptions.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: Gamma syntactically derives A
Means: There is a natural-deduction derivation of A whose undischarged assumptions all belong to Gamma.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: A is derivable without undischarged assumptions
Means: There is a derivation of A with no undischarged assumptions.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: conjunction introduction rule
Means: The natural-deduction rule that infers A and B from separate derivations of A and B.
Why this reading: The Open Logic macro expands to the printed name of an inference rule; the result is a rule label, not a formula using that connective.
Read as: formula D
Means: The metavariable D denotes an arbitrary formula.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: C and D
Means: The conjunction of formulas C and D.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: D and C
Means: The conjunction of formulas D and C, in that order.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: assumption C, labeled one for discharge
Means: An occurrence of assumption C marked with discharge label one.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: if C, then C and D
Means: The conditional with antecedent C and consequent the conjunction of C and D.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: assumption D, labeled one for discharge
Means: An occurrence of assumption D marked with discharge label one.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: if D, then C and D
Means: The conditional with antecedent D and consequent the conjunction of C and D.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from D, one can derive: if C, then C and D
Means: There is a natural-deduction derivation of the conditional from C to C and D using D as its only possible undischarged assumption.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from C, one can derive: if D, then C and D
Means: There is a natural-deduction derivation of the conditional from D to C and D using C as its only possible undischarged assumption.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: if A and B, then A
Means: The conditional whose antecedent is the conjunction A and B and whose consequent is A.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: if A and B, then A
Means: The conditional whose antecedent is the conjunction A and B and whose consequent is A.
Why this reading: This source shape differs from shape 032 only in source whitespace; both intentionally share the same display, speech, and meaning.
Read as: the single assumption that is the conjunction of A and B, labeled one for discharge
Means: An occurrence of the conjunctive assumption A and B marked with discharge label one.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: if either not A or B, then if A, then B
Means: A conditional from the disjunction not A or B to the conditional from A to B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: the single assumption that is the disjunction of not A with B, labeled one for discharge
Means: An occurrence of the disjunctive assumption not A or B marked with discharge label one.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: the disjunction of not A with B
Means: The disjunction whose left disjunct is not A and whose right disjunct is B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: assumption not A, labeled two for discharge
Means: An occurrence of assumption not A marked with discharge label two.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: assumption B, labeled two for discharge
Means: An occurrence of assumption B marked with discharge label two.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: assumptions not A labeled two, and A labeled three, for discharge
Means: Two active assumptions: not A carries discharge label two, while A carries discharge label three.
Why this reading: The two superscripts are separate discharge labels attached to separate assumptions.
Read as: assumptions B labeled two, and A labeled four, for discharge
Means: Two active assumptions: B carries discharge label two, while A carries discharge label four.
Why this reading: The two superscripts are separate discharge labels attached to separate assumptions.
Read as: assumption A, labeled three for discharge
Means: An occurrence of assumption A marked with discharge label three.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: A or not A
Means: The instance of excluded middle asserting the disjunction of A with its negation.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: disjunction introduction rule
Means: The natural-deduction rule that infers A or B from either A or B as a premise.
Why this reading: The Open Logic macro expands to the printed name of an inference rule; the result is a rule label, not a formula using that connective.
Read as: assumption denying the whole disjunction A or not A, labeled one for discharge
Means: An occurrence of the assumption denying the entire excluded-middle formula A or not A, marked with discharge label one.
Why this reading: The negation scopes over the complete disjunction, and the superscript one is its discharge label.
Read as: not the whole disjunction A or not A
Means: The negation of the complete excluded-middle formula A or not A.
Why this reading: The negation applies to the entire parenthesized disjunction.
Read as: negation elimination rule
Means: The natural-deduction rule that infers a contradiction from A together with not A.
Why this reading: The Open Logic macro expands to the printed name of an inference rule; the result is a rule label, not a formula using that connective.
Read as: two assumptions for discharge: the first denies the entire disjunction A or not A and is labeled one; the second is A and is labeled two
Means: Two active assumptions: the negation of the complete disjunction A or not A carries label one, and A carries label two.
Why this reading: The negation scopes over the whole first disjunction; the superscripts are separate discharge labels.
Read as: assumption A, labeled two for discharge
Means: An occurrence of assumption A marked with discharge label two.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: assumption not A, labeled three for discharge
Means: An occurrence of assumption not A marked with discharge label three.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: from the single conjunctive premise whose left conjunct is A and whose right conjunct is the conjunction of B and C, derive the conjunction of A and B, conjoined with C
Means: There is a derivation of the conjunction of A and B, conjoined with C, from the single assumption A conjoined with the conjunction of B and C.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from the disjunction whose left disjunct is A and whose right disjunct is the disjunction B or C, derive the disjunction whose left disjunct is A or B and whose right disjunct is C
Means: There is a derivation of the disjunction of A and B, disjoined with C, from the single assumption A disjoined with the disjunction of B and C.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from if A then if B then C, derive: if B then if A then C
Means: The sequent asserting that the two antecedents of a nested conditional may be exchanged by natural deduction.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from A, derive not not A
Means: The sequent asserting double-negation introduction: A has a derivation of not not A.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from if A or B then C, derive: if A then C
Means: The sequent asserting that the conditional from A or B to C yields a conditional from A to C.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from the conjunction of the conditional from A to C with the conditional from B to C, derive the conditional from the disjunction A or B to C
Means: From the single conjunctive assumption consisting of if A then C and if B then C, natural deduction derives the conditional from A or B to C.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: without undischarged assumptions, derive not both A and not A
Means: The law of noncontradiction has a natural-deduction derivation with no undischarged assumptions.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from if B then A, derive: if not A then not B
Means: The sequent expresses contraposition from the conditional B to A to the conditional not A to not B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: without undischarged assumptions, derive: if the conditional from A to not A holds, then not A
Means: The displayed conditional has a natural-deduction derivation with no undischarged assumptions.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: without undischarged assumptions, derive: if it is not the case that A implies B, then not B
Means: The displayed conditional from the negation of A implies B to not B has a derivation with no undischarged assumptions.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from if A then C, derive not both A and not C
Means: The sequent asserts that the conditional from A to C derives the negation of the conjunction A and not C.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from the conjunction of A with not C, derive that it is not the case that if A then C
Means: The sequent asserts that A together with not C derives the negation of the conditional from A to C.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from A or B, together with not B, derive A
Means: The sequent is disjunctive syllogism: A or B and not B derive A.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from the disjunction of not A with not B, derive not both A and B
Means: The sequent asserts that the disjunction of not A and not B derives the negation of A and B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: without undischarged assumptions, derive: if both not A and not B, then it is not the case that A or B
Means: One direction of De Morgan's law has a derivation without undischarged assumptions: not A and not B implies the negation of A or B.
Why this reading: In the consequent, negation scopes over the complete disjunction A or B.
Read as: without undischarged assumptions, derive: if it is not the case that A or B, then both not A and not B
Means: The converse De Morgan direction has a derivation without undischarged assumptions: the negation of A or B implies not A and not B.
Why this reading: The antecedent negation scopes over the complete disjunction A or B.
Read as: from the negation of if A then B, derive A
Means: The sequent asserts that denying the conditional from A to B yields a natural-deduction derivation of A.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from not both A and B, derive the disjunction of not A with not B
Means: The classical De Morgan sequent asserts that the negation of A and B derives the disjunction not A or not B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from the conditional if A then B, derive the disjunction of not A with B
Means: The sequent asserts the classical equivalence direction from a conditional to its material disjunction.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: without undischarged assumptions, derive: if not not A, then A
Means: Double-negation elimination has a classical natural-deduction derivation with no undischarged assumptions.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from two separate premises, the conditional from A to B and the conditional from not A to B, derive B
Means: The two conditionals to B, covering A and not A, jointly derive B by classical reasoning.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from if A and B then C, derive either if A then C or if B then C
Means: The classical sequent derives a disjunction of two conditionals from the conditional whose antecedent is A and B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: from the conditional whose antecedent is the conditional from A to B and whose consequent is A, derive A
Means: The sequent is the natural-deduction form of Peirce-style classical reasoning: the displayed premise derives A.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: without undischarged assumptions, derive either if A then B or if B then C
Means: The displayed disjunction of conditionals has a classical natural-deduction derivation with no undischarged assumptions.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: A is not derivable without undischarged assumptions
Means: There is no natural-deduction derivation of A with all assumptions discharged.
Why this reading: The slashed turnstile negates the complete derivability claim; it is not an inference arrow.
Read as: Gamma does not syntactically derive A
Means: There is no natural-deduction derivation of A whose undischarged assumptions all belong to Gamma.
Why this reading: The slashed turnstile negates the complete derivability-from-Gamma claim.
Read as: Gamma syntactically derives a contradiction
Means: There is a derivation of falsum whose undischarged assumptions are in Gamma.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: Gamma does not syntactically derive a contradiction
Means: There is no natural-deduction derivation of falsum from undischarged assumptions in Gamma; this expresses consistency of Gamma.
Why this reading: The slashed turnstile negates derivability of falsum and therefore expresses proof-theoretic consistency.
Read as: A is a member of Gamma
Means: Formula A belongs to the assumption set Gamma.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: Gamma is a subset of capital Delta
Means: Every formula in assumption set Gamma also belongs to assumption set Delta.
Why this reading: Capital Delta denotes a set of assumptions here and is distinct from lowercase delta used for a derivation.
Read as: capital Delta syntactically derives A
Means: There is a natural-deduction derivation of A whose undischarged assumptions all belong to the set Delta.
Why this reading: Capital Delta is an assumption set, not the lowercase delta notation for a derivation.
Read as: capital Delta
Means: Delta denotes a set of formulas used as undischarged assumptions.
Why this reading: The uppercase Greek letter denotes an assumption set and must not be confused with lowercase delta naming a derivation.
Read as: A together with capital Delta syntactically derives B
Means: There is a derivation of B whose undischarged assumptions lie in the union of Delta with the singleton set containing A.
Why this reading: The braces form the singleton set containing A; capital Delta is an assumption set.
Read as: the combined assumptions Gamma and capital Delta syntactically derive B
Means: There is a derivation of B whose undischarged assumptions lie in the union of Gamma and Delta.
Why this reading: The union applies to two assumption sets before the derivability relation is evaluated.
Read as: derivation delta zero
Means: Lowercase delta zero names the derivation of A from Gamma used in the local proof construction.
Why this reading: This is lowercase delta naming a derivation, with subscript zero; it is distinct from capital Delta, an assumption set.
Read as: delta one
Means: The first subderivation, named delta one.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: assumption A together with capital Delta
Means: The union of the singleton set containing formula A with the assumption set Delta.
Why this reading: The braces form a singleton set, and capital Delta denotes an assumption set.
Read as: capital Delta together with assumption A, labeled one for discharge
Means: The open assumptions in Delta together with an occurrence of assumption A carrying discharge label one.
Why this reading: Capital Delta is an assumption set; the superscript one labels only assumption A for discharge.
Read as: the union of Gamma and capital Delta
Means: The set containing every assumption that belongs to Gamma or to Delta.
Why this reading: Both Greek capitals denote sets of assumptions; the symbol forms their set-theoretic union.
Read as: Gamma equals the finite set containing A sub one, A sub two, through A sub k
Means: Gamma is being presented as the finite set of formulas A sub one through A sub k.
Why this reading: The subscripts index formulas; the braces are printed set braces and the ellipsis continues the indexed list.
Read as: from A sub one, A sub two, through A sub k, derive B
Means: B is derivable in natural deduction from the listed formulas A sub one through A sub k.
Why this reading: The turnstile denotes the natural-deduction derivability relation; it is not a conditional arrow or semantic entailment.
Read as: Gamma syntactically derives B
Means: There is a natural-deduction derivation of B whose undischarged assumptions all belong to Gamma.
Why this reading: The turnstile denotes the natural-deduction derivability relation; it is not a conditional arrow or semantic entailment.
Read as: from A, derive B
Means: B is derivable in natural deduction with A as the only possible undischarged assumption.
Why this reading: The turnstile denotes the natural-deduction derivability relation; it is not a conditional arrow or semantic entailment.
Read as: from the singleton set containing A, derive B
Means: B is derivable from the assumption set whose sole member is A.
Why this reading: These braces are printed singleton-set braces, unlike the nonprinting TeX grouping braces in shapes 098 through 100.
Read as: from A sub one through A sub n, derive B
Means: B is derivable in natural deduction from the finite list of formulas A sub one through A sub n.
Why this reading: The turnstile denotes the natural-deduction derivability relation; it is not a conditional arrow or semantic entailment.
Read as: Gamma syntactically derives A sub i
Means: The indexed formula A sub i is derivable from the assumption set Gamma.
Why this reading: The subscript i selects one member of the indexed formula family; the turnstile denotes derivability.
Read as: index i
Means: The index i ranges over the formulas in the finite premise list.
Why this reading: In this context i is an index, not a formula or an individual variable in the object language.
Read as: Gamma syntactically derives A
Means: Formula A is derivable from the assumption set Gamma.
Why this reading: The braces in the source are TeX grouping braces and do not print as set braces.
Read as: formula A
Means: A denotes an arbitrary sentence in the stated inconsistency condition.
Why this reading: The braces in the source are TeX grouping braces and do not print as set braces.
Read as: Gamma syntactically derives not A
Means: The negation of A is derivable from the assumption set Gamma.
Why this reading: The source braces only group A for TeX; the negation applies to A and the turnstile denotes derivability.
Read as: Gamma sub zero is a subset of Gamma
Means: Every formula in the finite assumption set Gamma sub zero also belongs to Gamma.
Why this reading: The zero is a subscript naming a selected finite subset, not a numerical value of Gamma.
Read as: Gamma sub zero syntactically derives A
Means: A is derivable from the finite assumption set Gamma sub zero.
Why this reading: The turnstile denotes the natural-deduction derivability relation; it is not a conditional arrow or semantic entailment.
Read as: delta
Means: Delta names the derivation under discussion.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: Gamma sub zero
Means: Gamma sub zero denotes the finite set of undischarged assumptions selected from Gamma.
Why this reading: The subscript zero identifies the selected finite assumption set.
Read as: formula A is syntactically identical to falsum
Means: The formula denoted by A is the falsum formula; this is the special case used in the compactness argument.
Why this reading: The equivalence-shaped symbol expresses syntactic identity of expressions here, not a biconditional inside the object language.
Read as: Gamma together with assumption A
Means: The union of Gamma with the singleton set containing formula A.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: delta two
Means: The second subderivation, named delta two.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: the assumptions in Gamma, together with assumption A labeled one for discharge
Means: A proof context containing the undischarged assumptions in Gamma and an occurrence of assumption A marked for discharge by a later discharging inference carrying label one.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: Gamma union the singleton set containing not A
Means: The assumption set obtained by adding the negated formula not A to Gamma.
Why this reading: The printed braces form a singleton set, and the negation applies only to A.
Read as: the assumptions in Gamma, together with assumption not A labeled one for discharge
Means: A proof context containing Gamma and an occurrence of the assumption not A marked with discharge label one.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: Gamma syntactically derives not A
Means: The negation of A is derivable from the assumption set Gamma.
Why this reading: The turnstile denotes the natural-deduction derivability relation; it is not a conditional arrow or semantic entailment.
Read as: not A is a member of Gamma
Means: The negated formula not A belongs to the assumption set Gamma.
Why this reading: No unresolved pronunciation, grouping, role, or scope ambiguity remains after inspection of every recorded source context.
Read as: Gamma union the singleton set containing A
Means: The assumption set obtained by adding formula A to Gamma.
Why this reading: The braces are printed singleton-set braces; source spacing does not change the set operation.
Read as: Gamma union the singleton set containing not A
Means: The assumption set obtained by adding the negated formula not A to Gamma.
Why this reading: This source shape differs from shape 109 only in whitespace; both have the same printed set-theoretic meaning.
Read as: the assumptions in Gamma, together with assumption not A labeled two for discharge
Means: A proof context containing Gamma and an occurrence of assumption not A marked with discharge label two.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: not not A
Means: The double negation of formula A.
Why this reading: Both negation operators apply successively to A; this is not a cancellation performed in the notation.
Read as: syntactic derivability
Means: The turnstile symbol denotes the natural-deduction derivability relation.
Why this reading: The turnstile denotes the natural-deduction derivability relation; it is not a conditional arrow or semantic entailment.
Read as: from the conjunction A and B, derive A
Means: The conjunction A and B derives its left conjunct A.
Why this reading: No unresolved pronunciation, grouping, role, or scope ambiguity remains after inspection of every recorded source context.
Read as: from two separate premises, A and the conditional from A to B, derive B
Means: A together with the conditional from A to B derives B by conditional elimination.
Why this reading: The comma separates two assumptions; the turnstile scopes over the complete premise list.
Read as: from the conjunction A and B, derive B
Means: The conjunction A and B derives its right conjunct B.
Why this reading: No unresolved pronunciation, grouping, role, or scope ambiguity remains after inspection of every recorded source context.
Read as: from A and B as separate assumptions, derive the conjunction A and B
Means: The separate assumptions A and B jointly derive their conjunction.
Why this reading: The comma to the left of the turnstile separates assumptions, while the conjunction to the right forms one formula.
Read as: the set of three assumptions: first, the disjunction A or B; second, not A; and third, not B
Means: The three-formula assumption set consisting of A or B, not A, and not B; the surrounding proposition states that it is inconsistent.
Why this reading: The commas list three assumptions; no derivability claim is contained inside this expression.
Read as: from A, derive A or B
Means: A derives the disjunction A or B by disjunction introduction.
Why this reading: No unresolved pronunciation, grouping, role, or scope ambiguity remains after inspection of every recorded source context.
Read as: from B, derive A or B
Means: B derives the disjunction A or B by disjunction introduction.
Why this reading: No unresolved pronunciation, grouping, role, or scope ambiguity remains after inspection of every recorded source context.
Read as: assumption A labeled one for discharge
Means: An occurrence of assumption A marked with discharge label one.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: not B
Means: The negation of formula B.
Why this reading: No unresolved pronunciation, grouping, role, or scope ambiguity remains after inspection of every recorded source context.
Read as: assumption B labeled one for discharge
Means: An occurrence of assumption B marked with discharge label one.
Why this reading: The superscript is an assumption-discharge label, not exponentiation or a proof-step number.
Read as: from not A, derive: if A then B
Means: The negation of A derives the conditional from A to B by assuming A, deriving a contradiction, and then deriving B.
Why this reading: No unresolved pronunciation, grouping, role, or scope ambiguity remains after inspection of every recorded source context.
Read as: from B, derive: if A then B
Means: B derives the conditional from A to B; conditional introduction need not discharge an occurrence of A.
Why this reading: No unresolved pronunciation, grouping, role, or scope ambiguity remains after inspection of every recorded source context.
Read as: Gamma semantically entails A
Means: Every structure that satisfies all assumptions in Gamma also satisfies formula A.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: zero
Means: The number zero.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: valuation v
Means: The fraktur letter v names a propositional truth-value assignment.
Why this reading: The styled v is a valuation, not an ordinary object-language variable.
Read as: n
Means: The number n of inferences in the derivation.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: Gamma together with assumption A, labeled n for discharge
Means: The open assumptions Gamma together with an occurrence of assumption A labeled n; the final negation-introduction inference discharges the assumption carrying that label.
Why this reading: The superscript n is a discharge label, not a temporal step number.
Read as: valuation v satisfies every formula in Gamma
Means: Every formula in the assumption set Gamma is true under propositional valuation v.
Why this reading: This is the semantic satisfaction relation for a propositional valuation, not syntactic derivability.
Read as: valuation v satisfies not A
Means: The negation of A is true under propositional valuation v.
Why this reading: This is the semantic satisfaction relation for a propositional valuation, not syntactic derivability.
Read as: valuation v does not satisfy not A
Means: The negation of A is not true under propositional valuation v.
Why this reading: The slashed satisfaction relation negates the entire claim that valuation v satisfies not A.
Read as: valuation v satisfies A
Means: Formula A is true under propositional valuation v.
Why this reading: This is the semantic satisfaction relation for a propositional valuation, not syntactic derivability.
Read as: valuation v satisfies every formula in Gamma together with A
Means: Valuation v makes true every formula in the set obtained by adding A to Gamma.
Why this reading: Satisfaction applies to the complete union of Gamma with the singleton set containing A.
Read as: Gamma semantically entails A and B
Means: Every structure satisfying Gamma satisfies the conjunction of A and B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: valuation v satisfies A and B
Means: The conjunction A and B is true under propositional valuation v.
Why this reading: This is the semantic satisfaction relation for a propositional valuation, not syntactic derivability.
Read as: valuation v satisfies B
Means: Formula B is true under propositional valuation v.
Why this reading: This is the semantic satisfaction relation for a propositional valuation, not syntactic derivability.
Read as: valuation v satisfies A or B
Means: The disjunction A or B is true under propositional valuation v.
Why this reading: This is the semantic satisfaction relation for a propositional valuation, not syntactic derivability.
Read as: Gamma together with assumption A semantically entails B
Means: Every structure satisfying Gamma and A also satisfies B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: Gamma semantically entails: if A, then B
Means: Every structure satisfying Gamma satisfies the conditional from A to B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: valuation v does not satisfy the conditional from A to B
Means: The conditional from A to B is false under propositional valuation v.
Why this reading: The slashed satisfaction relation negates satisfaction of the complete conditional.
Read as: valuation v does not satisfy B
Means: Formula B is false under propositional valuation v.
Why this reading: The slashed satisfaction relation states that B is not true under valuation v.
Read as: Gamma semantically entails a contradiction
Means: Every structure satisfying Gamma would have to satisfy falsum.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: valuation v does not satisfy A
Means: Formula A is false under propositional valuation v.
Why this reading: The slashed satisfaction relation states that A is not true under valuation v.
Read as: valuation v does not satisfy falsum
Means: Falsum is false under propositional valuation v.
Why this reading: The slashed satisfaction statement records the defining impossibility of satisfying falsum.
Read as: Gamma does not semantically entail a contradiction
Means: It is not the case that every structure satisfying Gamma satisfies falsum.
Why this reading: The slash on entailment negates the whole semantic-consequence claim.
Read as: Gamma one
Means: The first set of undischarged assumptions.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: Gamma two
Means: The second set of undischarged assumptions.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: the combined assumptions Gamma one and Gamma two
Means: The union of the two sets of undischarged assumptions.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: the combined assumptions Gamma one and Gamma two semantically entail A and B
Means: Every structure satisfying both assumption sets satisfies the conjunction of A and B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: valuation v satisfies every formula in Gamma sub one union Gamma sub two
Means: Valuation v makes true every formula belonging to either assumption set Gamma sub one or Gamma sub two.
Why this reading: The satisfaction relation applies to the union of the two indexed assumption sets.
Read as: valuation v satisfies every formula in Gamma sub one
Means: Every formula in assumption set Gamma sub one is true under valuation v.
Why this reading: This is the semantic satisfaction relation for a propositional valuation, not syntactic derivability.
Read as: Gamma one semantically entails A
Means: Every structure satisfying Gamma one satisfies A.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: valuation v satisfies every formula in Gamma sub two
Means: Every formula in assumption set Gamma sub two is true under valuation v.
Why this reading: This is the semantic satisfaction relation for a propositional valuation, not syntactic derivability.
Read as: Gamma two semantically entails B
Means: Every structure satisfying Gamma two satisfies B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: Gamma one semantically entails: if A, then B
Means: Every structure satisfying Gamma one satisfies the conditional from A to B.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.
Read as: valuation v satisfies the conditional from A to B
Means: The conditional from A to B is true under propositional valuation v.
Why this reading: This is the semantic satisfaction relation for a propositional valuation, not syntactic derivability.
Read as: Gamma two semantically entails A
Means: Every structure satisfying Gamma two satisfies A.
Why this reading: No unresolved pronunciation or scope ambiguity is recorded for this expression.