The Open Logic Text — accessible offline edition

Syntax and Semantics — Explore equations

Syntax and Semantics

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

Equation and object guide

Every distinct expression in Syntax and Semantics appears with navigable MathML, reviewed speech and meaning, and every source occurrence.

154 expression records

Expression 3

v1¯\pValue{v_1}

Conventional reading: evaluation function induced by valuation v sub 1

Meaning here: The evaluation function induced by valuation v sub 1; it extends the assignment on sentence letters to every formula.

1 occurrence
  1. Occurrence 1: valuations-sat.tex, line 138, column 24

Expression 4

((¬(p0→p1)→(p0∨p1))∧¬(p0∧p1))(( \lnot ( \Obj p_0 \lif \Obj p_1 ) \lif ( \Obj p_0 \lor \Obj p_1 )) \land \lnot ( \Obj p_0 \land \Obj p_1 ))

Conventional reading: open parenthesis open parenthesis not open parenthesis sentence letter p sub 0 implies sentence letter p sub 1 close parenthesis implies open parenthesis sentence letter p sub 0 or sentence letter p sub 1 close parenthesis close parenthesis and not open parenthesis sentence letter p sub 0 and sentence letter p sub 1 close parenthesis close parenthesis

Meaning here: A conjunction whose left conjunct is a conditional from the negated p-zero-to-p-one conditional to the p-zero-or-p-one disjunction, and whose right conjunct negates p zero and p one.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 110, column 11

Expression 5

Ai≡¬Aj!A_i \ident \lnot !A_j

Conventional reading: A sub i is syntactically identical to not A sub j

Meaning here: The statement read 'A sub i is syntactically identical to not A sub j' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 28, column 22

Expression 6

v:Prop→{True,False}\pAssign{v} \colon \PVar \to \{\True, \False \}

Conventional reading: valuation v colon the set of propositional variables maps to open set brace true comma false close set brace

Meaning here: Valuation v is a function from the set of propositional variables to the two-element set containing true and false.

1 occurrence
  1. Occurrence 1: valuations-sat.tex, line 17, column 52

Expression 8

A[[B1/p1],…,[Bn/pn]]\SSubst{!A}{\subst{!B_1}{\Obj p_1},\dots,\subst{!B_n}{\Obj p_n}}

Conventional reading: the result of simultaneous substitution in A using B sub 1 for sentence letter p sub 1 comma and so on comma B sub n for sentence letter p sub n

Meaning here: The expression read 'the result of simultaneous substitution in A using B sub 1 for sentence letter p sub 1 comma and so on comma B sub n for sentence letter p sub n' specifies a substitution of formulas for propositional variables; the spoken order states what is inserted, what it replaces, and where.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 97, column 1

Expression 9

v2¯\pValue{v_2}

Conventional reading: evaluation function induced by valuation v sub 2

Meaning here: The evaluation function induced by valuation v sub 2; it extends the assignment on sentence letters to every formula.

1 occurrence
  1. Occurrence 1: valuations-sat.tex, line 138, column 43

Expression 10

Δ⊨A\Delta \Entails !A

Conventional reading: capital Delta semantically entails A

Meaning here: The statement read 'capital Delta semantically entails A' says that every propositional valuation satisfying all premises on the left also satisfies the conclusion on the right.

1 occurrence
  1. Occurrence 1: semantic-notions.tex, line 55, column 38

Expression 13

(Aj∧Ak)(!A_j \land !A_k)

Conventional reading: open parenthesis A sub j and A sub k close parenthesis

Meaning here: The conjunction of indexed formulas A sub j and A sub k, with its outer parentheses shown.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 149, column 1

Expression 14

{True,False}\{\True, \False\}

Conventional reading: open set brace true comma false close set brace

Meaning here: The two-element set of propositional truth values: true and false.

1 occurrence
  1. Occurrence 1: valuations-sat.tex, line 14, column 5

Expression 17

¬\neg

Conventional reading: not sign

Meaning here: The not sign used as a notation variant for propositional negation; it is distinct from the tilde variant.

1 occurrence
  1. Occurrence 1: formulas.tex, line 66, column 9

Expression 20

v\pAssign{v}

Conventional reading: valuation v

Meaning here: The fraktur letter v names a propositional truth-value assignment.

11 occurrences
  1. Occurrence 1: introduction.tex, line 54, column 49
  2. Occurrence 2: introduction.tex, line 58, column 16
  3. Occurrence 3: introduction.tex, line 68, column 34
  4. Occurrence 4: valuations-sat.tex, line 16, column 10
  5. Occurrence 5: valuations-sat.tex, line 22, column 24
  6. Occurrence 6: valuations-sat.tex, line 149, column 18
  7. Occurrence 7: semantic-notions.tex, line 18, column 8
  8. Occurrence 8: semantic-notions.tex, line 19, column 34
  9. Occurrence 9: semantic-notions.tex, line 21, column 22
  10. Occurrence 10: semantic-notions.tex, line 26, column 17
  11. Occurrence 11: semantic-notions.tex, line 28, column 49

Expression 22

An≡¬Aj!A_n \ident \lnot !A_j

Conventional reading: A sub n is syntactically identical to not A sub j

Meaning here: The statement read 'A sub n is syntactically identical to not A sub j' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 134, column 22

Expression 23

FrmL0⊆S\Frm[L_0] \subseteq S

Conventional reading: the set of formulas of language L sub 0 is a subset of S

Meaning here: Every formula of language L sub 0 belongs to the set S.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 37, column 31

Expression 24

Γ∪{A}⊨B\Gamma \cup \{!A\} \Entails !B

Conventional reading: Gamma together with assumption A semantically entails B

Meaning here: Every structure satisfying Gamma and A also satisfies B.

1 occurrence
  1. Occurrence 1: semantic-notions.tex, line 85, column 6

Expression 25

An≡(Aj∨Ak)!A_n \ident (!A_j \lor !A_k)

Conventional reading: A sub n is syntactically identical to open parenthesis A sub j or A sub k close parenthesis

Meaning here: The statement read 'A sub n is syntactically identical to open parenthesis A sub j or A sub k close parenthesis' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 136, column 21

Expression 27

(p0→(¬p1→¬p0))( \Obj p_0 \lif ( \lnot \Obj p_1 \lif \lnot \Obj p_0 ) )

Conventional reading: open parenthesis sentence letter p sub 0 implies open parenthesis not sentence letter p sub 1 implies not sentence letter p sub 0 close parenthesis close parenthesis

Meaning here: A conditional from sentence letter p sub 0 to the conditional from not p sub 1 to not p sub 0.

1 occurrence
  1. Occurrence 1: semantic-notions.tex, line 38, column 9

Expression 29

⇔\Leftrightarrow

Conventional reading: double arrow biconditional symbol

Meaning here: The expression read 'double arrow biconditional symbol' is a notation variant discussed for a propositional connective or syntactic relation; its spoken form names the role rather than relying on the glyph.

1 occurrence
  1. Occurrence 1: formulas.tex, line 71, column 3

Expression 30

⊃\supset

Conventional reading: horseshoe conditional symbol

Meaning here: The expression read 'horseshoe conditional symbol' is a notation variant discussed for a propositional connective or syntactic relation; its spoken form names the role rather than relying on the glyph.

1 occurrence
  1. Occurrence 1: formulas.tex, line 68, column 55

Expression 33

j,k<ij,k < i

Conventional reading: indices j and k are less than i

Meaning here: The condition read 'indices j and k are less than i' constrains indices so that cited formulas occur earlier in a finite formation sequence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 25, column 51

Expression 34

v1¯(A)=v2¯(A)\pValue{v_1}(!A) = \pValue{v_2}(!A)

Conventional reading: truth value of A under valuation v sub 1 equals truth value of A under valuation v sub 2

Meaning here: The evaluation functions induced by valuations v sub 1 and v sub 2 assign the same truth value to formula A.

1 occurrence
  1. Occurrence 1: valuations-sat.tex, line 139, column 16

Expression 37

∅⊨A\emptyset \Entails !A

Conventional reading: the empty premise set semantically entails A

Meaning here: Formula A follows semantically from no premises, so A is true under every propositional valuation.

1 occurrence
  1. Occurrence 1: semantic-notions.tex, line 49, column 3

Expression 38

⟨B0,…,Bn,C0,…,Cm,(Bn→Cm)⟩\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \lif !C_m)}

Conventional reading: sequence B sub 0 comma and so on comma B sub n comma C sub 0 comma and so on comma C sub m comma open parenthesis B sub n implies C sub m close parenthesis

Meaning here: The sequence read 'sequence B sub 0 comma and so on comma B sub n comma C sub 0 comma and so on comma C sub m comma open parenthesis B sub n implies C sub m close parenthesis' is a finite formation sequence whose earlier entries justify the construction of its final propositional formula.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 87, column 12

Expression 39

((p0∨p1)∧p2)( ( \Obj p_0 \lor \Obj p_1 ) \land \Obj p_2 )

Conventional reading: open parenthesis open parenthesis sentence letter p sub 0 or sentence letter p sub 1 close parenthesis and sentence letter p sub 2 close parenthesis

Meaning here: The conjunction of the disjunction of p sub 0 with p sub 1 and the sentence letter p sub 2.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 108, column 11

Expression 41

v¯:FrmL0→{True,False}\pValue{v} \colon \Frm[L_0] \to \{\True, \False \}

Conventional reading: evaluation function induced by valuation v, from formulas of language L sub 0 to the truth values true and false

Meaning here: The evaluation function induced by valuation v maps every formula of language L sub 0 to either true or false.

1 occurrence
  1. Occurrence 1: valuations-sat.tex, line 23, column 3

Expression 43

Prop\PVar

Conventional reading: the set of propositional variables

Meaning here: The set of all propositional variables, or sentence letters, in the language.

1 occurrence
  1. Occurrence 1: formulas.tex, line 21, column 29

Expression 44

(B∗C)(!B \ast !C)

Conventional reading: open parenthesis B binary connective star C close parenthesis

Meaning here: The fully parenthesized result of applying an arbitrary binary connective to formulas B and C.

1 occurrence
  1. Occurrence 1: formulas.tex, line 129, column 24

Expression 46

pn∈Prop\Obj p_n \in \PVar

Conventional reading: sentence letter p sub n is a member of the set of propositional variables

Meaning here: Sentence letter p sub n is a member of the set of propositional variables.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 66, column 27

Expression 48

(A→B)∧(B→A)(!A \lif !B) \land (!B \lif !A)

Conventional reading: open parenthesis A implies B close parenthesis and open parenthesis B implies A close parenthesis

Meaning here: The conjunction of the conditional from A to B and the converse conditional from B to A.

1 occurrence
  1. Occurrence 1: formulas.tex, line 161, column 44

Expression 49

(¬p0∧p0)( \lnot \Obj p_0 \land \Obj p_0 )

Conventional reading: open parenthesis not sentence letter p sub 0 and sentence letter p sub 0 close parenthesis

Meaning here: The contradictory conjunction of not p sub 0 with p sub 0.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 107, column 11

Expression 52

v¯(⊥)=False;v¯(pn)=v(pn);v¯(¬A)={Trueif v¯(A)=False;Falseotherwise.v¯(A∧B)={Trueif v¯(A)=True and v¯(B)=True;Falseif v¯(A)=False or v¯(B)=False.v¯(A∨B)={Trueif v¯(A)=True or v¯(B)=True;Falseif v¯(A)=False and v¯(B)=False.v¯(A→B)={Trueif v¯(A)=False or v¯(B)=True;Falseif v¯(A)=True and v¯(B)=False.\pValue{v}(\lfalse) & = \False; \\ \pValue{v}(\Obj p_n) & = \pAssign{v}(\Obj p_n); \\ \pValue{v}(\lnot !A) & = \begin{cases} \True & \text{if } \pValue{v}(!A) = \False;\\ \False & \text{otherwise.} \end{cases} \\ \pValue{v}(!A \land !B) & = \begin{cases} \True & \text{if $\pValue{v}(!A) = \True$ and $\pValue{v}(!B) = \True$;}\\ \False & \text{if $\pValue{v}(!A) = \False$ or $\pValue{v}(!B) = \False$}. \end{cases}\\ \pValue{v}(!A \lor !B) & = \begin{cases} \True & \text{if $\pValue{v}(!A) = \True$ or $\pValue{v}(!B) = \True$;}\\ \False & \text{if $\pValue{v}(!A) = \False$ and $\pValue{v}(!B) = \False$}. \end{cases}\\ \pValue{v}(!A \lif !B) & = \begin{cases} \True & \text{if $\pValue{v}(!A) = \False$ or $\pValue{v}(!B) = \True$;}\\ \False & \text{if $\pValue{v}(!A) = \True$ and $\pValue{v}(!B) = \False$}. \end{cases}\\

Conventional reading: Truth value clauses. Falsum is false. A sentence letter has the value assigned to it. Not A is true exactly when A is false. A and B is true exactly when both A and B are true. A or B is true exactly when at least one of A and B is true. If A, then B is false exactly when A is true and B is false.

Meaning here: The recursive truth definition for falsum, sentence letters, negation, conjunction, disjunction, and the material conditional under propositional valuation v.

1 occurrence
  1. Occurrence 1: valuations-sat.tex, line 24, column 3

Expression 53

An≡(Aj→Ak)!A_n \ident (!A_j \lif !A_k)

Conventional reading: A sub n is syntactically identical to open parenthesis A sub j implies A sub k close parenthesis

Meaning here: The statement read 'A sub n is syntactically identical to open parenthesis A sub j implies A sub k close parenthesis' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 137, column 21

Expression 54

¬((p0→p1)∧p2)\lnot ( ( \Obj p_0 \lif \Obj p_1 ) \land \Obj p_2 )

Conventional reading: not open parenthesis open parenthesis sentence letter p sub 0 implies sentence letter p sub 1 close parenthesis and sentence letter p sub 2 close parenthesis

Meaning here: The negation of the conjunction whose conjuncts are the conditional from p sub 0 to p sub 1 and sentence letter p sub 2.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 109, column 11

Expression 56

Γ\Gamma

Conventional reading: Gamma, a set of formulas

Meaning here: An arbitrary set Gamma of propositional formulas, used as premises in satisfaction and semantic consequence.

9 occurrences
  1. Occurrence 1: introduction.tex, line 70, column 35
  2. Occurrence 2: valuations-sat.tex, line 182, column 4
  3. Occurrence 3: semantic-notions.tex, line 24, column 10
  4. Occurrence 4: semantic-notions.tex, line 24, column 69
  5. Occurrence 5: semantic-notions.tex, line 27, column 10
  6. Occurrence 6: semantic-notions.tex, line 27, column 45
  7. Occurrence 7: semantic-notions.tex, line 29, column 27
  8. Occurrence 8: semantic-notions.tex, line 52, column 10
  9. Occurrence 9: semantic-notions.tex, line 52, column 62

Expression 57

i≤ni \leq n

Conventional reading: i is less than or equal to n

Meaning here: The condition read 'i is less than or equal to n' constrains indices so that cited formulas occur earlier in a finite formation sequence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 24, column 52

Expression 58

k≤nk \leq n

Conventional reading: k is less than or equal to n

Meaning here: The condition read 'k is less than or equal to n' constrains indices so that cited formulas occur earlier in a finite formation sequence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 106, column 22

Expression 59

v¯(A)\pValue{v}(!A)

Conventional reading: truth value of A under valuation v

Meaning here: The truth value assigned to formula A by the evaluation function induced by valuation v.

1 occurrence
  1. Occurrence 1: introduction.tex, line 56, column 40

Expression 60

True\True

Conventional reading: true

Meaning here: The truth value true.

24 occurrences
  1. Occurrence 1: introduction.tex, line 27, column 24
  2. Occurrence 2: introduction.tex, line 55, column 14
  3. Occurrence 3: valuations-sat.tex, line 16, column 41
  4. Occurrence 4: valuations-sat.tex, line 66, column 5
  5. Occurrence 5: valuations-sat.tex, line 67, column 16
  6. Occurrence 6: valuations-sat.tex, line 75, column 5
  7. Occurrence 7: valuations-sat.tex, line 75, column 15
  8. Occurrence 8: valuations-sat.tex, line 75, column 25
  9. Occurrence 9: valuations-sat.tex, line 76, column 5
  10. Occurrence 10: valuations-sat.tex, line 77, column 16
  11. Occurrence 11: valuations-sat.tex, line 86, column 5
  12. Occurrence 12: valuations-sat.tex, line 86, column 15
  13. Occurrence 13: valuations-sat.tex, line 86, column 25
  14. Occurrence 14: valuations-sat.tex, line 87, column 5
  15. Occurrence 15: valuations-sat.tex, line 87, column 26
  16. Occurrence 16: valuations-sat.tex, line 88, column 16
  17. Occurrence 17: valuations-sat.tex, line 88, column 26
  18. Occurrence 18: valuations-sat.tex, line 98, column 5
  19. Occurrence 19: valuations-sat.tex, line 98, column 15
  20. Occurrence 20: valuations-sat.tex, line 98, column 25
  21. Occurrence 21: valuations-sat.tex, line 99, column 5
  22. Occurrence 22: valuations-sat.tex, line 100, column 16
  23. Occurrence 23: valuations-sat.tex, line 100, column 26
  24. Occurrence 24: valuations-sat.tex, line 101, column 27

Expression 64

∼\sim

Conventional reading: tilde negation symbol

Meaning here: The expression read 'tilde negation symbol' is a notation variant discussed for a propositional connective or syntactic relation; its spoken form names the role rather than relying on the glyph.

1 occurrence
  1. Occurrence 1: formulas.tex, line 66, column 1

Expression 65

FrmL0=S\Frm[L_0] = S

Conventional reading: the set of formulas of language L sub 0 equals S

Meaning here: The set of all formulas of language L sub 0 is exactly the set S.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 37, column 59

Expression 66

An≡(Aj∧Ak)!A_n \ident (!A_j \land !A_k)

Conventional reading: A sub n is syntactically identical to open parenthesis A sub j and A sub k close parenthesis

Meaning here: The statement read 'A sub n is syntactically identical to open parenthesis A sub j and A sub k close parenthesis' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 135, column 22

Expression 68

v⊨A\pSat{v}{!A}

Conventional reading: valuation v satisfies A

Meaning here: Formula A is true under propositional valuation v.

10 occurrences
  1. Occurrence 1: introduction.tex, line 59, column 9
  2. Occurrence 2: introduction.tex, line 64, column 43
  3. Occurrence 3: valuations-sat.tex, line 149, column 34
  4. Occurrence 4: valuations-sat.tex, line 150, column 43
  5. Occurrence 5: valuations-sat.tex, line 183, column 1
  6. Occurrence 6: valuations-sat.tex, line 187, column 3
  7. Occurrence 7: semantic-notions.tex, line 18, column 23
  8. Occurrence 8: semantic-notions.tex, line 19, column 49
  9. Occurrence 9: semantic-notions.tex, line 20, column 51
  10. Occurrence 10: semantic-notions.tex, line 25, column 34

Expression 70

(B'→C')(!B' \lif !C')

Conventional reading: open parenthesis B prime implies C prime close parenthesis

Meaning here: The conditional from primed formula B to primed formula C, with its outer parentheses shown.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 83, column 32

Expression 72

FrmL0\Frm[L_0]

Conventional reading: the set of formulas of language L sub 0

Meaning here: The set of all well-formed formulas of propositional language L sub 0.

8 occurrences
  1. Occurrence 1: formulas.tex, line 80, column 9
  2. Occurrence 2: preliminaries.tex, line 36, column 56
  3. Occurrence 3: preliminaries.tex, line 42, column 23
  4. Occurrence 4: preliminaries.tex, line 59, column 25
  5. Occurrence 5: formation-sequences.tex, line 65, column 27
  6. Occurrence 6: formation-sequences.tex, line 116, column 1
  7. Occurrence 7: formation-sequences.tex, line 129, column 44
  8. Occurrence 8: formation-sequences.tex, line 147, column 52

Expression 73

((¬p0→p1)∧p2)( ( \lnot \Obj p_0 \lif \Obj p_1 ) \land \Obj p_2 )

Conventional reading: open parenthesis open parenthesis not sentence letter p sub 0 implies sentence letter p sub 1 close parenthesis and sentence letter p sub 2 close parenthesis

Meaning here: The conjunction of the conditional from not p sub 0 to p sub 1 and sentence letter p sub 2.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 103, column 21

Expression 74

⟨B0,…,Bn,C0,…,Cm,(Bn∧Cm)⟩\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \land !C_m)}

Conventional reading: sequence B sub 0 comma and so on comma B sub n comma C sub 0 comma and so on comma C sub m comma open parenthesis B sub n and C sub m close parenthesis

Meaning here: The sequence read 'sequence B sub 0 comma and so on comma B sub n comma C sub 0 comma and so on comma C sub m comma open parenthesis B sub n and C sub m close parenthesis' is a finite formation sequence whose earlier entries justify the construction of its final propositional formula.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 81, column 12

Expression 76

↔\leftrightarrow

Conventional reading: left right arrow biconditional symbol

Meaning here: The expression read 'left right arrow biconditional symbol' is a notation variant discussed for a propositional connective or syntactic relation; its spoken form names the role rather than relying on the glyph.

1 occurrence
  1. Occurrence 1: formulas.tex, line 70, column 37

Expression 77

Ai≡(Aj∨Ak)!A_i \ident (!A_j \lor !A_k)

Conventional reading: A sub i is syntactically identical to open parenthesis A sub j or A sub k close parenthesis

Meaning here: The statement read 'A sub i is syntactically identical to open parenthesis A sub j or A sub k close parenthesis' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 30, column 21

Expression 78

¬(p1∧p0)\lnot (\Obj p_1 \land \Obj p_0)

Conventional reading: not open parenthesis sentence letter p sub 1 and sentence letter p sub 0 close parenthesis

Meaning here: The negation of the conjunction of sentence letters p sub 1 and p sub 0.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 46, column 1

Expression 79

Ai≡(Aj→Ak)!A_i \ident (!A_j \lif !A_k)

Conventional reading: A sub i is syntactically identical to open parenthesis A sub j implies A sub k close parenthesis

Meaning here: The statement read 'A sub i is syntactically identical to open parenthesis A sub j implies A sub k close parenthesis' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 31, column 21

Expression 80

A!A

Conventional reading: formula A

Meaning here: The metavariable A denotes an arbitrary formula.

48 occurrences
  1. Occurrence 1: introduction.tex, line 57, column 13
  2. Occurrence 2: introduction.tex, line 60, column 18
  3. Occurrence 3: introduction.tex, line 62, column 26
  4. Occurrence 4: introduction.tex, line 70, column 59
  5. Occurrence 5: formulas.tex, line 90, column 21
  6. Occurrence 6: formulas.tex, line 93, column 21
  7. Occurrence 7: formulas.tex, line 96, column 20
  8. Occurrence 8: formulas.tex, line 99, column 20
  9. Occurrence 9: formulas.tex, line 169, column 35
  10. Occurrence 10: formulas.tex, line 175, column 9
  11. Occurrence 11: formulas.tex, line 178, column 45
  12. Occurrence 12: formulas.tex, line 179, column 14
  13. Occurrence 13: preliminaries.tex, line 19, column 11
  14. Occurrence 14: preliminaries.tex, line 21, column 29
  15. Occurrence 15: preliminaries.tex, line 23, column 29
  16. Occurrence 16: preliminaries.tex, line 25, column 29
  17. Occurrence 17: preliminaries.tex, line 59, column 17
  18. Occurrence 18: preliminaries.tex, line 82, column 17
  19. Occurrence 19: preliminaries.tex, line 82, column 50
  20. Occurrence 20: preliminaries.tex, line 85, column 35
  21. Occurrence 21: preliminaries.tex, line 92, column 4
  22. Occurrence 22: preliminaries.tex, line 94, column 69
  23. Occurrence 23: preliminaries.tex, line 102, column 8
  24. Occurrence 24: formation-sequences.tex, line 24, column 15
  25. Occurrence 25: formation-sequences.tex, line 65, column 19
  26. Occurrence 26: formation-sequences.tex, line 69, column 9
  27. Occurrence 27: formation-sequences.tex, line 70, column 24
  28. Occurrence 28: formation-sequences.tex, line 79, column 35
  29. Occurrence 29: formation-sequences.tex, line 82, column 35
  30. Occurrence 30: formation-sequences.tex, line 85, column 35
  31. Occurrence 31: formation-sequences.tex, line 88, column 35
  32. Occurrence 32: formation-sequences.tex, line 126, column 9
  33. Occurrence 33: formation-sequences.tex, line 146, column 5
  34. Occurrence 34: valuations-sat.tex, line 64, column 5
  35. Occurrence 35: valuations-sat.tex, line 73, column 5
  36. Occurrence 36: valuations-sat.tex, line 84, column 5
  37. Occurrence 37: valuations-sat.tex, line 96, column 5
  38. Occurrence 38: valuations-sat.tex, line 136, column 25
  39. Occurrence 39: valuations-sat.tex, line 138, column 13
  40. Occurrence 40: valuations-sat.tex, line 139, column 4
  41. Occurrence 41: valuations-sat.tex, line 143, column 17
  42. Occurrence 42: valuations-sat.tex, line 148, column 38
  43. Occurrence 43: valuations-sat.tex, line 191, column 19
  44. Occurrence 44: semantic-notions.tex, line 17, column 21
  45. Occurrence 45: semantic-notions.tex, line 20, column 21
  46. Occurrence 46: semantic-notions.tex, line 22, column 21
  47. Occurrence 47: semantic-notions.tex, line 25, column 11
  48. Occurrence 48: semantic-notions.tex, line 48, column 7

Expression 81

A[B/p]\Subst{!A}{!B}{p}

Conventional reading: the result of substituting B for p in A

Meaning here: The expression read 'the result of substituting B for p in A' specifies a substitution of formulas for propositional variables; the spoken order states what is inserted, what it replaces, and where.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 115, column 46

Expression 82

v¯(◇(A,B,C))={v¯(B)if v¯(A)=True;v¯(C)if v¯(A)=False.\pValue{v}(\diamondsuit( !A , !B , !C ) ) = \begin{cases} \pValue{v}( !B ) & \text{if $\pValue{v}(!A) = \True$;}\\ \pValue{v}( !C ) & \text{if $\pValue{v}(!A) = \False $}. \end{cases}

Conventional reading: The truth value of diamond applied to A, B, and C is the truth value of B when A is true, and is the truth value of C when A is false.

Meaning here: A proposed ternary connective that selects its second argument when the first argument is true and its third argument when the first argument is false.

1 occurrence
  1. Occurrence 1: valuations-sat.tex, line 122, column 1

Expression 83

A≡B!A \ident !B

Conventional reading: A is syntactically identical to B

Meaning here: The statement read 'A is syntactically identical to B' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formulas.tex, line 169, column 16

Expression 84

A≡An!A \ident !A_n

Conventional reading: A is syntactically identical to A sub n

Meaning here: The statement read 'A is syntactically identical to A sub n' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 24, column 23

Expression 85

·\cdot

Conventional reading: centered dot conjunction symbol

Meaning here: The expression read 'centered dot conjunction symbol' is a notation variant discussed for a propositional connective or syntactic relation; its spoken form names the role rather than relying on the glyph.

1 occurrence
  1. Occurrence 1: formulas.tex, line 66, column 52

Expression 87

Γ∪Δ⊨B\Gamma \cup \Delta \Entails !B

Conventional reading: Gamma union capital Delta semantically entails B

Meaning here: The statement read 'Gamma union capital Delta semantically entails B' says that every propositional valuation satisfying all premises on the left also satisfies the conclusion on the right.

1 occurrence
  1. Occurrence 1: semantic-notions.tex, line 57, column 42

Expression 89

→\rightarrow

Conventional reading: right arrow conditional symbol

Meaning here: The expression read 'right arrow conditional symbol' is a notation variant discussed for a propositional connective or syntactic relation; its spoken form names the role rather than relying on the glyph.

1 occurrence
  1. Occurrence 1: formulas.tex, line 68, column 21

Expression 90

Δ∪{A}⊨B\Delta \cup \{ !A\} \Entails !B

Conventional reading: capital Delta union open set brace A close set brace semantically entails B

Meaning here: The statement read 'capital Delta union open set brace A close set brace semantically entails B' says that every propositional valuation satisfying all premises on the left also satisfies the conclusion on the right.

1 occurrence
  1. Occurrence 1: semantic-notions.tex, line 57, column 3

Expression 93

&\&

Conventional reading: ampersand conjunction symbol

Meaning here: The expression read 'ampersand conjunction symbol' is a notation variant discussed for a propositional connective or syntactic relation; its spoken form names the role rather than relying on the glyph.

1 occurrence
  1. Occurrence 1: formulas.tex, line 66, column 65

Expression 94

⟨C0,…,Cm⟩\tuple{!C_0,\dotsc,!C_m}

Conventional reading: sequence C sub 0 comma and so on comma C sub m

Meaning here: The sequence read 'sequence C sub 0 comma and so on comma C sub m' is a finite formation sequence whose earlier entries justify the construction of its final propositional formula.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 73, column 32

Expression 95

v⊨current induction-case formula\pSat{v}{\indfrm}

Conventional reading: valuation v satisfies the current induction-case formula

Meaning here: A context-sensitive satisfaction statement whose current induction-case formula is expanded in each occurrence.

5 occurrences
  1. Occurrence 1: valuations-sat.tex, line 158, column 30
  2. Occurrence 2: valuations-sat.tex, line 162, column 26
  3. Occurrence 3: valuations-sat.tex, line 166, column 31
  4. Occurrence 4: valuations-sat.tex, line 170, column 30
  5. Occurrence 5: valuations-sat.tex, line 174, column 30

Expression 97

Γ⊨B\Gamma \Entails !B

Conventional reading: Gamma semantically entails B

Meaning here: The statement read 'Gamma semantically entails B' says that every propositional valuation satisfying all premises on the left also satisfies the conclusion on the right.

1 occurrence
  1. Occurrence 1: semantic-notions.tex, line 51, column 3

Expression 98

⟨A⟩\tuple{!A}

Conventional reading: sequence A

Meaning here: The sequence read 'sequence A' is a finite formation sequence whose earlier entries justify the construction of its final propositional formula.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 69, column 43

Expression 99

A≡(Aj∧Ak)!A \equiv (!A_j \land !A_k)

Conventional reading: A is syntactically identical to open parenthesis A sub j and A sub k close parenthesis

Meaning here: The statement read 'A is syntactically identical to open parenthesis A sub j and A sub k close parenthesis' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 141, column 44

Expression 101

Γ∪{¬A}\Gamma \cup \{\lnot !A\}

Conventional reading: Gamma union the singleton set containing not A

Meaning here: The assumption set obtained by adding the negated formula not A to Gamma.

1 occurrence
  1. Occurrence 1: semantic-notions.tex, line 71, column 39

Expression 102

B∗C!B \ast !C

Conventional reading: B binary connective star C

Meaning here: The result of applying an arbitrary binary connective to formulas B and C without outer parentheses.

1 occurrence
  1. Occurrence 1: formulas.tex, line 131, column 48

Expression 103

(¬p0∧p1)( \lnot \Obj p_0 \land \Obj p_1)

Conventional reading: open parenthesis not sentence letter p sub 0 and sentence letter p sub 1 close parenthesis

Meaning here: The conjunction of not p sub 0 with sentence letter p sub 1.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 102, column 45

Expression 105

(p0↔p1)→(p2↔¬p1)( \Obj p_0 \liff \Obj p_1 ) \lif ( \Obj p_2 \liff \lnot \Obj p_1 )

Conventional reading: open parenthesis sentence letter p sub 0 if and only if sentence letter p sub 1 close parenthesis implies open parenthesis sentence letter p sub 2 if and only if not sentence letter p sub 1 close parenthesis

Meaning here: A conditional from the biconditional between p sub 0 and p sub 1 to the biconditional between p sub 2 and not p sub 1.

1 occurrence
  1. Occurrence 1: semantic-notions.tex, line 40, column 9

Expression 106

Γ⊨A\Gamma \Entails !A

Conventional reading: Gamma semantically entails A

Meaning here: Every structure that satisfies all assumptions in Gamma also satisfies formula A.

6 occurrences
  1. Occurrence 1: introduction.tex, line 69, column 22
  2. Occurrence 2: semantic-notions.tex, line 24, column 45
  3. Occurrence 3: semantic-notions.tex, line 50, column 10
  4. Occurrence 4: semantic-notions.tex, line 55, column 7
  5. Occurrence 5: semantic-notions.tex, line 56, column 42
  6. Occurrence 6: semantic-notions.tex, line 71, column 3

Expression 108

⟨A0,…,Aj⟩\tuple{!A_0,\dotsc,!A_j}

Conventional reading: sequence A sub 0 comma and so on comma A sub j

Meaning here: The sequence read 'sequence A sub 0 comma and so on comma A sub j' is a finite formation sequence whose earlier entries justify the construction of its final propositional formula.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 143, column 1

Expression 109

⇒\Rightarrow

Conventional reading: double right arrow conditional symbol

Meaning here: The expression read 'double right arrow conditional symbol' is a notation variant discussed for a propositional connective or syntactic relation; its spoken form names the role rather than relying on the glyph.

1 occurrence
  1. Occurrence 1: formulas.tex, line 68, column 36

Expression 110

j,k<nj,k < n

Conventional reading: indices j and k are less than n

Meaning here: The condition read 'indices j and k are less than n' constrains indices so that cited formulas occur earlier in a finite formation sequence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 131, column 28

Expression 112

An∈FrmL0!A_n \in \Frm[L_0]

Conventional reading: A sub n is a member of the set of formulas of language L sub 0

Meaning here: The indexed string A sub n is a well-formed formula of language L sub 0.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 141, column 1

Expression 115

⟨B0,…,Bn,¬Bn⟩\tuple{!B_0,\dotsc,!B_n,\lnot !B_n}

Conventional reading: sequence B sub 0 comma and so on comma B sub n comma not B sub n

Meaning here: The sequence read 'sequence B sub 0 comma and so on comma B sub n comma not B sub n' is a finite formation sequence whose earlier entries justify the construction of its final propositional formula.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 78, column 12

Expression 116

v⊭current induction-case formula\pSat/{v}{\indfrm}

Conventional reading: valuation v does not satisfy the current induction-case formula

Meaning here: A context-sensitive non-satisfaction statement whose current induction-case formula is expanded in this occurrence.

1 occurrence
  1. Occurrence 1: valuations-sat.tex, line 153, column 25

Expression 117

⟨p0,p1,p0,(p1∧p0),(p0→p1),¬(p1∧p0)⟩.\tuple{ \Obj p_0, \Obj p_1, \Obj p_0, (\Obj p_1 \land \Obj p_0), (\Obj p_0 \lif \Obj p_1), \lnot (\Obj p_1 \land \Obj p_0) }.

Conventional reading: sequence sentence letter p sub 0 comma sentence letter p sub 1 comma sentence letter p sub 0 comma open parenthesis sentence letter p sub 1 and sentence letter p sub 0 close parenthesis comma open parenthesis sentence letter p sub 0 implies sentence letter p sub 1 close parenthesis comma not open parenthesis sentence letter p sub 1 and sentence letter p sub 0 close parenthesis

Meaning here: The sequence read 'sequence sentence letter p sub 0 comma sentence letter p sub 1 comma sentence letter p sub 0 comma open parenthesis sentence letter p sub 1 and sentence letter p sub 0 close parenthesis comma open parenthesis sentence letter p sub 0 implies sentence letter p sub 1 close parenthesis comma not open parenthesis sentence letter p sub 1 and sentence letter p sub 0 close parenthesis' is a finite formation sequence whose earlier entries justify the construction of its final propositional formula.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 47, column 1

Expression 119

S⊆FrmL0S \subseteq \Frm[L_0]

Conventional reading: S is a subset of the set of formulas of language L sub 0

Meaning here: Every member of S is a well-formed formula of language L sub 0.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 34, column 25

Expression 122

((p0↔(¬p1∧p2))∨(p2→(p0↔p1)))(( \Obj p_0 \liff ( \lnot \Obj p_1 \land \Obj p_2 )) \lor ( \Obj p_2 \lif ( \Obj p_0 \liff \Obj p_1 )))

Conventional reading: open parenthesis open parenthesis sentence letter p sub 0 if and only if open parenthesis not sentence letter p sub 1 and sentence letter p sub 2 close parenthesis close parenthesis or open parenthesis sentence letter p sub 2 implies open parenthesis sentence letter p sub 0 if and only if sentence letter p sub 1 close parenthesis close parenthesis close parenthesis

Meaning here: A disjunction whose left disjunct is the biconditional between p sub 0 and the conjunction of not p sub 1 with p sub 2, and whose right disjunct is a conditional from p sub 2 to the biconditional between p sub 0 and p sub 1.

1 occurrence
  1. Occurrence 1: semantic-notions.tex, line 41, column 9

Expression 125

⟨B0,…,Bn,C0,…,Cm,(Bn∨Cm)⟩\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \lor !C_m)}

Conventional reading: sequence B sub 0 comma and so on comma B sub n comma C sub 0 comma and so on comma C sub m comma open parenthesis B sub n or C sub m close parenthesis

Meaning here: The sequence read 'sequence B sub 0 comma and so on comma B sub n comma C sub 0 comma and so on comma C sub m comma open parenthesis B sub n or C sub m close parenthesis' is a finite formation sequence whose earlier entries justify the construction of its final propositional formula.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 84, column 12

Expression 127

((p0∧¬p1)→(¬p0∧p2))↔((p2→p0)→(p0→p1))( ( \Obj p_0 \land \lnot \Obj p_1 ) \lif ( \lnot \Obj p_0 \land \Obj p_2 )) \liff ( ( \Obj p_2 \lif \Obj p_0 ) \lif ( \Obj p_0 \lif \Obj p_1 ))

Conventional reading: open parenthesis open parenthesis sentence letter p sub 0 and not sentence letter p sub 1 close parenthesis implies open parenthesis not sentence letter p sub 0 and sentence letter p sub 2 close parenthesis close parenthesis if and only if open parenthesis open parenthesis sentence letter p sub 2 implies sentence letter p sub 0 close parenthesis implies open parenthesis sentence letter p sub 0 implies sentence letter p sub 1 close parenthesis close parenthesis

Meaning here: A biconditional between a conditional from p-zero-and-not-p-one to not-p-zero-and-p-two, and a nested conditional from p-two-implies-p-zero to p-zero-implies-p-one.

1 occurrence
  1. Occurrence 1: semantic-notions.tex, line 39, column 9

Expression 129

A≡(B∧C)!A \ident (!B \land !C)

Conventional reading: A is syntactically identical to open parenthesis B and C close parenthesis

Meaning here: The statement read 'A is syntactically identical to open parenthesis B and C close parenthesis' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 80, column 23

Expression 131

⟨B0,…,Bn⟩\tuple{!B_0,\dotsc,!B_n}

Conventional reading: sequence B sub 0 comma and so on comma B sub n

Meaning here: The sequence read 'sequence B sub 0 comma and so on comma B sub n' is a finite formation sequence whose earlier entries justify the construction of its final propositional formula.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 73, column 1

Expression 132

∧\wedge

Conventional reading: wedge conjunction symbol

Meaning here: The expression read 'wedge conjunction symbol' is a notation variant discussed for a propositional connective or syntactic relation; its spoken form names the role rather than relying on the glyph.

1 occurrence
  1. Occurrence 1: formulas.tex, line 66, column 42

Expression 136

B!B

Conventional reading: formula B

Meaning here: The metavariable B denotes an arbitrary formula.

22 occurrences
  1. Occurrence 1: introduction.tex, line 62, column 35
  2. Occurrence 2: formulas.tex, line 93, column 30
  3. Occurrence 3: formulas.tex, line 96, column 29
  4. Occurrence 4: formulas.tex, line 99, column 29
  5. Occurrence 5: formulas.tex, line 129, column 56
  6. Occurrence 6: formulas.tex, line 169, column 44
  7. Occurrence 7: formulas.tex, line 176, column 36
  8. Occurrence 8: formulas.tex, line 179, column 28
  9. Occurrence 9: preliminaries.tex, line 21, column 38
  10. Occurrence 10: preliminaries.tex, line 23, column 38
  11. Occurrence 11: preliminaries.tex, line 25, column 38
  12. Occurrence 12: preliminaries.tex, line 68, column 50
  13. Occurrence 13: preliminaries.tex, line 70, column 56
  14. Occurrence 14: preliminaries.tex, line 72, column 54
  15. Occurrence 15: preliminaries.tex, line 74, column 54
  16. Occurrence 16: preliminaries.tex, line 83, column 55
  17. Occurrence 17: preliminaries.tex, line 92, column 13
  18. Occurrence 18: preliminaries.tex, line 94, column 61
  19. Occurrence 19: formation-sequences.tex, line 72, column 18
  20. Occurrence 20: valuations-sat.tex, line 73, column 12
  21. Occurrence 21: valuations-sat.tex, line 84, column 12
  22. Occurrence 22: valuations-sat.tex, line 96, column 12

Expression 138

⟨p0,p1,(p1∧p0),¬(p1∧p0)⟩\tuple{ \Obj p_0, \Obj p_1, (\Obj p_1 \land \Obj p_0), \lnot (\Obj p_1 \land \Obj p_0) }

Conventional reading: sequence sentence letter p sub 0 comma sentence letter p sub 1 comma open parenthesis sentence letter p sub 1 and sentence letter p sub 0 close parenthesis comma not open parenthesis sentence letter p sub 1 and sentence letter p sub 0 close parenthesis

Meaning here: The sequence read 'sequence sentence letter p sub 0 comma sentence letter p sub 1 comma open parenthesis sentence letter p sub 1 and sentence letter p sub 0 close parenthesis comma not open parenthesis sentence letter p sub 1 and sentence letter p sub 0 close parenthesis' is a finite formation sequence whose earlier entries justify the construction of its final propositional formula.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 37, column 1

Expression 140

Ai≡(Aj∧Ak)!A_i \ident (!A_j \land !A_k)

Conventional reading: A sub i is syntactically identical to open parenthesis A sub j and A sub k close parenthesis

Meaning here: The statement read 'A sub i is syntactically identical to open parenthesis A sub j and A sub k close parenthesis' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 29, column 22

Expression 142

≡\equiv

Conventional reading: triple bar biconditional symbol

Meaning here: The triple-bar symbol as a notation variant for the material biconditional in the source's notation comparison.

1 occurrence
  1. Occurrence 1: formulas.tex, line 71, column 26

Expression 143

FrmL0⊆F\Frm[L_0] \subseteq F

Conventional reading: the set of formulas of language L sub 0 is a subset of F

Meaning here: Every formula of language L sub 0 belongs to the set F of strings having formation sequences.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 124, column 1

Expression 145

(B∧C)(!B \land !C)

Conventional reading: open parenthesis B and C close parenthesis

Meaning here: The conjunction of formulas B and C, with its outer parentheses shown.

1 occurrence
  1. Occurrence 1: preliminaries.tex, line 70, column 18

Expression 146

A≡¬B!A \ident \lnot !B

Conventional reading: A is syntactically identical to not B

Meaning here: The statement read 'A is syntactically identical to not B' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 77, column 23

Expression 148

A≡(B→C)!A \ident (!B \lif !C)

Conventional reading: A is syntactically identical to open parenthesis B implies C close parenthesis

Meaning here: The statement read 'A is syntactically identical to open parenthesis B implies C close parenthesis' compares symbol strings for exact syntactic identity, not merely equal truth value or logical equivalence.

1 occurrence
  1. Occurrence 1: formation-sequences.tex, line 86, column 22

Expression 149

False\False

Conventional reading: false

Meaning here: The truth value false.

22 occurrences
  1. Occurrence 1: introduction.tex, line 27, column 44
  2. Occurrence 2: introduction.tex, line 55, column 23
  3. Occurrence 3: valuations-sat.tex, line 16, column 52
  4. Occurrence 4: valuations-sat.tex, line 66, column 15
  5. Occurrence 5: valuations-sat.tex, line 67, column 5
  6. Occurrence 6: valuations-sat.tex, line 76, column 15
  7. Occurrence 7: valuations-sat.tex, line 76, column 26
  8. Occurrence 8: valuations-sat.tex, line 77, column 5
  9. Occurrence 9: valuations-sat.tex, line 77, column 26
  10. Occurrence 10: valuations-sat.tex, line 78, column 5
  11. Occurrence 11: valuations-sat.tex, line 78, column 16
  12. Occurrence 12: valuations-sat.tex, line 78, column 27
  13. Occurrence 13: valuations-sat.tex, line 87, column 15
  14. Occurrence 14: valuations-sat.tex, line 88, column 5
  15. Occurrence 15: valuations-sat.tex, line 89, column 5
  16. Occurrence 16: valuations-sat.tex, line 89, column 16
  17. Occurrence 17: valuations-sat.tex, line 89, column 27
  18. Occurrence 18: valuations-sat.tex, line 99, column 15
  19. Occurrence 19: valuations-sat.tex, line 99, column 26
  20. Occurrence 20: valuations-sat.tex, line 100, column 5
  21. Occurrence 21: valuations-sat.tex, line 101, column 5
  22. Occurrence 22: valuations-sat.tex, line 101, column 16

Expression 150

v1(pn)=v2(pn)\pAssign{v_1}(\Obj p_n) = \pAssign{v_2}(\Obj p_n)

Conventional reading: valuation v sub 1 applied to sentence letter p sub n equals valuation v sub 2 applied to sentence letter p sub n

Meaning here: Valuations v sub 1 and v sub 2 assign the same truth value to sentence letter p sub n.

1 occurrence
  1. Occurrence 1: valuations-sat.tex, line 136, column 37

Expression 151

v(pi)=True\pAssign{v}(\Obj p_i) = \True

Conventional reading: valuation v applied to sentence letter p sub i equals true

Meaning here: Valuation v assigns truth value true to sentence letter p sub i.

1 occurrence
  1. Occurrence 1: valuations-sat.tex, line 159, column 7

Four truth tables

Negation truth table

Negation truth table
Anot A
TrueFalse
FalseTrue

Words-only linearization: Negation truth table. Row one. A is true. Not A is false. Row two. A is false. Not A is true.

Conjunction truth table

Conjunction truth table
ABA and B
TrueTrueTrue
TrueFalseFalse
FalseTrueFalse
FalseFalseFalse

Words-only linearization: Conjunction truth table. Row one. A is true. B is true. A and B is true. Row two. A is true. B is false. A and B is false. Row three. A is false. B is true. A and B is false. Row four. A is false. B is false. A and B is false.

Disjunction truth table

Disjunction truth table
ABA or B
TrueTrueTrue
TrueFalseTrue
FalseTrueTrue
FalseFalseFalse

Words-only linearization: Disjunction truth table. Row one. A is true. B is true. A or B is true. Row two. A is true. B is false. A or B is true. Row three. A is false. B is true. A or B is true. Row four. A is false. B is false. A or B is false.

Material conditional truth table

Material conditional truth table
ABif A then B
TrueTrueTrue
TrueFalseFalse
FalseTrueTrue
FalseFalseTrue

Words-only linearization: Material conditional truth table. Row one. A is true. B is true. If A, then B is true. Row two. A is true. B is false. If A, then B is false. Row three. A is false. B is true. If A, then B is true. Row four. A is false. B is false. If A, then B is true.

38 formal objects

  1. Definition: Propositional formulas — formulas.tex, line 78.
  2. Definition: Defined propositional operators — formulas.tex, line 134.
  3. Definition: Syntactic identity — formulas.tex, line 167.
  4. Theorem: Structural induction for formulas — preliminaries.tex, line 13.
  5. Proposition: Balanced parentheses in formulas — preliminaries.tex, line 41.
  6. Exercise: Prove balanced parentheses — preliminaries.tex, line 46.
  7. Proposition: No proper initial segment is a formula — preliminaries.tex, line 50.
  8. Exercise: Prove the initial-segment proposition — preliminaries.tex, line 54.
  9. Proposition: Unique readability of formulas — preliminaries.tex, line 58.
  10. Definition: Uniform substitution — preliminaries.tex, line 91.
  11. Exercise: Identify uniform substitutions — preliminaries.tex, line 100.
  12. Exercise: Define substitution by induction — preliminaries.tex, line 114.
  13. Definition: Formation sequences for formulas — formation-sequences.tex, line 20.
  14. Example: A formation sequence — formation-sequences.tex, line 36.
  15. Proposition: Every formula has a formation sequence — formation-sequences.tex, line 63.
  16. Lemma: Initial subsequences remain formation sequences — formation-sequences.tex, line 103.
  17. Theorem: Formulas characterized by formation sequences — formation-sequences.tex, line 114.
  18. Definition: Propositional valuations — valuations-sat.tex, line 13.
  19. Definition: Evaluation of propositional formulas — valuations-sat.tex, line 21.
  20. Display: Recursive evaluation clauses — valuations-sat.tex, line 24.
  21. Negation truth table — valuations-sat.tex, line 63.
  22. Conjunction truth table — valuations-sat.tex, line 72.
  23. Disjunction truth table — valuations-sat.tex, line 83.
  24. Material conditional truth table — valuations-sat.tex, line 95.
  25. Exercise: A ternary connective — valuations-sat.tex, line 119.
  26. Display: Evaluation of the ternary connective — valuations-sat.tex, line 122.
  27. Theorem: Local determination — valuations-sat.tex, line 133.
  28. Definition: Satisfaction by a valuation — valuations-sat.tex, line 146.
  29. Proposition: Satisfaction agrees with truth value — valuations-sat.tex, line 186.
  30. Exercise: Prove satisfaction agrees with truth value — valuations-sat.tex, line 194.
  31. Definition: Satisfiability, tautology, and semantic consequence — semantic-notions.tex, line 15.
  32. Exercise: Classify formulas semantically — semantic-notions.tex, line 34.
  33. Proposition: Basic semantic consequence facts — semantic-notions.tex, line 45.
  34. Exercise: Prove the semantic consequence facts — semantic-notions.tex, line 66.
  35. Proposition: Consequence and unsatisfiability — semantic-notions.tex, line 70.
  36. Exercise: Prove the consequence-unsatisfiability equivalence — semantic-notions.tex, line 79.
  37. Theorem: Semantic deduction theorem — semantic-notions.tex, line 83.
  38. Exercise: Prove the semantic deduction theorem — semantic-notions.tex, line 92.

9 resolved references

  1. Definition: Propositional formulas — preliminaries.tex, line 35.
  2. Proposition: Balanced parentheses in formulas — preliminaries.tex, line 47.
  3. Proposition: No proper initial segment is a formula — preliminaries.tex, line 55.
  4. Proposition: Every formula has a formation sequence — formation-sequences.tex, line 123.
  5. Lemma: Initial subsequences remain formation sequences — formation-sequences.tex, line 142.
  6. Proposition: Satisfaction agrees with truth value — valuations-sat.tex, line 195.
  7. Proposition: Basic semantic consequence facts — semantic-notions.tex, line 67.
  8. Proposition: Consequence and unsatisfiability — semantic-notions.tex, line 80.
  9. Theorem: Semantic deduction theorem — semantic-notions.tex, line 93.

Propositional Logic: introduction to this part