Fully Evaluated Left-Sequential Logics

Alban Ponse; Daan J.C. Staudt

arxiv: 2403.14576 · v2 · pith:YZ6PQ23Znew · submitted 2024-03-21 · 💻 cs.LO

Fully Evaluated Left-Sequential Logics

Alban Ponse , Daan J.C. Staudt This is my paper

Pith reviewed 2026-05-24 03:13 UTC · model grok-4.3

classification 💻 cs.LO

keywords left-sequential logicfully evaluatedevaluation treesaxiomatizationBochvar logicthree-valued logicpropositional expressionsconditional logic

0 comments

The pith

Four fully evaluated left-sequential logics form a hierarchy distinguished by memorization and conditionals, each with complete axiomatizations over evaluation trees.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines a family of two-valued logics that evaluate propositional expressions strictly left to right while differing in how they handle prior results and atomic side effects. Free FEL is the weakest and remains unaffected by side effects on atoms. Memorising FEL remembers subexpression values, Conditional FEL adds conditional behavior, and Static FEL is the strongest and reduces to a sequential version of ordinary propositional logic. Evaluation trees serve as the semantics, and each logic receives a complete axiomatization for closed terms. Three-valued extensions introduce an undefined constant U, supply two extra axioms each, and identify the strongest three-valued case with Bochvar's strict logic.

Core claim

The paper establishes four two-valued FELs ordered by strength: Free FEL (immune to atomic side effects), Memorising FEL (stores prior evaluations), Conditional FEL (incorporates conditional evaluation), and Static FEL (equivalent to sequential propositional logic). Evaluation trees provide the distinguishing semantics, and each logic has a complete axiomatization. The three-valued versions (with constant U) inherit the two-valued axioms plus two for undefinedness, and the strongest three-valued FEL coincides with Bochvar's strict logic.

What carries the argument

Evaluation trees, which encode the left-to-right evaluation steps of propositional expressions and separate the logics according to whether results are discarded, memorized, or conditioned.

If this is right

Any equivalence between closed terms that holds in a given FEL can be derived from its axioms.
The three-valued axiomatizations are sound and complete for reasoning with undefinedness under the respective sequential regimes.
Static FEL supplies a sequential presentation of Bochvar's strict logic.
The hierarchy isolates the minimal additions (memorization, conditionals) needed to recover classical behavior from a side-effect-free base.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

These systems could serve as precise models for short-circuit operators in programming languages where evaluation order and side effects matter.
The evaluation-tree semantics might extend to first-order or quantified sequential logics while preserving the completeness results.
Embedding the weaker FELs into the stronger ones could yield conservative extension theorems useful for stepwise verification.
The link to Bochvar's logic suggests possible translations between sequential undefinedness and other three-valued systems.

Load-bearing premise

That evaluation trees correctly and exhaustively capture the intended semantics of left-sequential evaluation without missing relevant distinctions or side-effect behaviors.

What would settle it

A closed term whose truth value or equivalence class under the axiomatization differs from the value obtained by direct traversal of its evaluation tree.

read the original abstract

We consider a family of two-valued "fully evaluated left-sequential logics" (FELs), of which Free FEL (defined by Staudt in 2012) is most distinguishing (weakest) and immune to atomic side effects. Next is Memorising FEL, in which evaluations of subexpressions are memorised. The following stronger logic is Conditional FEL (inspired by Guzm\'an and Squier's Conditional logic, 1990). The strongest FEL is static FEL, a sequential version of propositional logic. We use evaluation trees as a simple, intuitive semantics and provide complete axiomatisations for closed terms (left-sequential propositional expressions). For each FEL except Static FEL, we also define its three-valued version, with a constant U for "undefinedness" and again provide complete, independent axiomatisations, each one containing two additional axioms for U on top of the axiomatisations of the two-valued case. In this setting, the strongest FEL is equivalent to Bochvar's strict logic.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper defines a family of left-sequential propositional logics with axiomatizations for two- and three-valued cases, adding the memorising variant and showing equivalence of the strongest three-valued version to Bochvar's logic.

read the letter

The paper lays out four two-valued fully evaluated left-sequential logics ordered by strength: Free FEL (from Staudt 2012), Memorising FEL, Conditional FEL (building on Guzmán and Squier 1990), and Static FEL. It gives evaluation-tree semantics for each and supplies complete axiomatizations for closed terms. The three-valued versions add a constant U for undefinedness to the first three logics, each with two extra axioms, and the strongest three-valued case matches Bochvar's strict logic. The new pieces are the memorising variant and the explicit three-valued axiomatizations. The tree semantics is presented as a direct way to track left-to-right order and memorisation without side effects in the free case. The claims of completeness and independence rest on the supplied axiom lists plus the tree models; if the inductive arguments in the body hold, the results are on solid ground. The work stays within propositional logic and does not claim to solve open problems outside this setting. A minor soft spot is that the distinction between the four regimes depends entirely on how the trees are defined to encode memorisation versus non-memorisation, so the adequacy of that encoding is load-bearing. This is a technical contribution for people working on sequential or three-valued logics and their use in programming-language semantics. It is worth sending to peer review because the formal results are stated clearly and extend prior cited work without obvious circularity.

Referee Report

2 major / 0 minor

Summary. The manuscript defines a family of two-valued fully evaluated left-sequential logics (FELs): Free FEL (weakest, side-effect immune), Memorising FEL, Conditional FEL, and Static FEL (strongest, sequential propositional logic). It employs evaluation trees as semantics for closed left-sequential propositional expressions and asserts complete axiomatizations for each two-valued variant; for the three-valued versions (with undefinedness constant U) of the first three variants it supplies two additional axioms each and claims the strongest three-valued FEL coincides with Bochvar's strict logic.

Significance. If the completeness claims hold, the work supplies a uniform semantic and axiomatic treatment of left-sequential evaluation regimes that differ in memorization and side-effect handling, extending Staudt (2012) and Guzmán-Squier (1990). The evaluation-tree semantics is presented as intuitive and the independence of the added U axioms is a potential strength, but neither machine-checked proofs nor reproducible derivations are supplied.

major comments (2)

[Abstract] Abstract and main text: the central claim that complete axiomatizations are provided for each FEL variant (two-valued and three-valued) is unsupported because neither the explicit axiom sets nor any proof sketch (inductive argument that every tree-valid formula is derivable) appears in the manuscript; soundness and completeness therefore cannot be verified.
The load-bearing assumption that evaluation trees correctly distinguish the four evaluation regimes (Free, Memorising, Conditional, Static) and induce the intended consequence relations is stated but not accompanied by explicit verification or counter-example checks that would confirm the distinctions are non-trivial and that the strongest three-valued case is indeed Bochvar-strict.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. Below we respond point by point to the major comments and indicate the revisions we will make.

read point-by-point responses

Referee: [Abstract] Abstract and main text: the central claim that complete axiomatizations are provided for each FEL variant (two-valued and three-valued) is unsupported because neither the explicit axiom sets nor any proof sketch (inductive argument that every tree-valid formula is derivable) appears in the manuscript; soundness and completeness therefore cannot be verified.

Authors: We agree that the manuscript would benefit from greater explicitness. Although the abstract asserts that complete axiomatizations are supplied, the full axiom sets for each variant and the corresponding completeness proofs (or even sketches) are not presented in the main text. In the revised version we will list the complete axiom sets for Free FEL, Memorising FEL, Conditional FEL, Static FEL and the three-valued extensions, together with inductive proof sketches establishing that every evaluation-tree valid formula is derivable. revision: yes
Referee: [—] The load-bearing assumption that evaluation trees correctly distinguish the four evaluation regimes (Free, Memorising, Conditional, Static) and induce the intended consequence relations is stated but not accompanied by explicit verification or counter-example checks that would confirm the distinctions are non-trivial and that the strongest three-valued case is indeed Bochvar-strict.

Authors: The evaluation-tree semantics is defined so that the four regimes differ by construction in their handling of memorization and side effects. We nevertheless accept that explicit verification would strengthen the claim. In the revision we will add concrete counter-examples and small-model checks showing non-trivial distinctions among the four two-valued regimes and confirming that the strongest three-valued FEL coincides with Bochvar's strict logic. revision: yes

Circularity Check

0 steps flagged

Minor self-citation on base Free FEL definition; new axiomatizations and semantics are independent

full rationale

The manuscript defines four FEL variants and their three-valued extensions, supplies evaluation-tree semantics, and lists axiom sets claimed to be complete. The sole self-citation is the 2012 definition of Free FEL by co-author Staudt; this is used only as the starting point for the family and is not invoked to justify completeness or the claimed equivalence of static FEL to Bochvar's logic. No equation, prediction, or central claim reduces by construction to a quantity fitted or defined inside the present work, nor does any uniqueness theorem or ansatz rest on an unverified self-citation chain. The derivation therefore remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The central claims rest on the prior definitions of Free FEL and Conditional logic plus the new assumption that evaluation trees capture left-sequential behavior; no free parameters or invented physical entities appear.

axioms (1)

domain assumption Evaluation trees provide the semantics for left-sequential propositional expressions
Invoked to define the four FELs and to support completeness claims (abstract, paragraph 1)

invented entities (2)

Memorising FEL no independent evidence
purpose: Variant that stores results of evaluated subexpressions
Newly introduced in the family of FELs
Free FEL no independent evidence
purpose: Weakest variant immune to atomic side effects
Defined by reference to Staudt 2012 but positioned as base of the new family

pith-pipeline@v0.9.0 · 5703 in / 1224 out tokens · 56131 ms · 2026-05-24T03:13:20.876847+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages · 4 internal anchors

[1]

Bergstra, J.A., Bethke, I., and Rodenburg, P.H. (1995). A propositional logic with 4 values: true, false, divergent and meaningless, Journal of Applied Non-Classical Logics , 5(2):199-217. https://doi.org/10.1080/11663081.1995.10510855

work page doi:10.1080/11663081.1995.10510855 1995
[2]

Evaluation trees for proposition algebra

Bergstra, J.A. and Ponse, A. (2015). Evaluation trees fo r proposition algebra. https://doi.org/10.48550/arXiv.1504.08321 [cs.LO]

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1504.08321 2015
[3]

and Ponse, A

Bergstra, J.A. and Ponse, A. (2023). Conditional logic a s a short-circuit logic. https://doi.org/10.48550/arXiv.2304.14821 [cs.LO]

work page doi:10.48550/arxiv.2304.14821 2023
[4]

Short-circuit logic

Bergstra, J.A., Ponse, A., and Staudt, D.J.C. (2010 / 201 3). Short-circuit logic. (First version appeared in 2010.) https://doi.org/10.48550/arXiv.1010.3674 [cs.LO,math.LO]

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1010.3674 2010
[5]

Bergstra, J.A., Ponse, A., and Staudt, D.J.C. (2018). Pr opositional logic with short-circuit evaluation: a non-commutative and a commutative variant. https://doi.org/10.48550/arXiv.1810.02142 [cs.LO,math.LO]

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1810.02142 2018
[6]

Bergstra, J.A., Ponse, A., and Staudt, D.J.C. (2021). No n-commutative propositional logic with short- circuit evaluation. Journal of Applied Non-Classical Logics , 31(3-4):234-278 (online available). https://doi.org/10.1080/11663081.2021.2010954

work page doi:10.1080/11663081.2021.2010954 2021
[7]

Blok, A. (2011). Side-Eﬀecting Logic, [Unpublished manuscript], University of Amsterdam

work page 2011
[8]

Bochvar, D.A. (1938). On a 3-valued logical calculus and its application to the analysis of contradictions (in Russian). Matematicheskii Sbornik, 4(2):287-308

work page 1938
[9]

Contractive SCL

Burris, S.N. and Sankappanavar, H.P. (2012). A Course in Universal Algebra - The Millennium Edition . Available at http://www.math.uwaterloo.ca/~snburris/htdocs/ualg.html. 6Suppose A = {a}. Then there are 5 ·44 ·33 terms composed of four elements of {a,¬ a, a ∨q T, a ∧q F} and the three connectives in { ∧q , ∨q , ↔← } that have evaluation trees of depth 4...

work page 2012
[10]

Church, A. (1956). Introduction to Mathematical Logic . Princeton University Press

work page 1956
[11]

Cornets de Groot, S.H. (2012). Logical systems with lef t-sequential versions of NAND and XOR. MSc. thesis Logic, University of Amsterdam (June 2020). https://eprints.illc.uva.nl/id/eprint/1743/1/MoL-2020-02.text.pdf

work page 2012
[12]

and Squier, C.C

Guzm´ an, F. and Squier, C.C. (1990). The algebra of cond itional logic. Algebra Universalis , 27:88-110. https://doi.org/10.1007/BF01190256

work page doi:10.1007/bf01190256 1990
[13]

Hoare, C.A.R. (1985). A couple of novelties in the propo sitional calculus. Zeitschrift f¨ ur Mathematische Logik und Grundlagen der Mathematik , 31(2):173-178. https://doi.org/10.1002/malq.19850310905

work page doi:10.1002/malq.19850310905 1985
[14]

Kleene, S.C. (1938). On a notation for ordinal numbers. Journal of Symbolic Logic , 3:150-155

work page 1938
[15]

McCarthy, J. (1963). A basis for a mathematical theory o f computation. In P. Braﬀort and D. Hirschberg (eds.), Computer Programming and Formal Systems , pages 33–70, North-Holland, Amsterdam

work page 1963
[16]

McCune W. (2008). The GUI: Prover9 and Mace4 with a graph ical user interface. Prover9-Mace4 Version 0.5B. (Prover9-Mace4-v05B.zip, March 14, 2008). https://www.cs.unm.edu/~mccune/prover9/gui/v05.html

work page 2008
[17]

and Ponse, A

Papuc, D. and Ponse, A. (2022). Non-commutative propos itional logic with short-circuited biconditional and NAND. https://doi.org/10.48550/arXiv.2203.09321 [cs.LO]

work page doi:10.48550/arxiv.2203.09321 2022
[18]

and Staudt, D.J.C

Ponse, A. and Staudt, D.J.C. (2018). An independent axi omatisation for free short-circuit logic. Journal of Applied Non-Classical Logics , 28(1), 35-71 (online available). https://doi.org/10.1080/11663081.2018.1448637

work page doi:10.1080/11663081.2018.1448637 2018
[19]

Staudt, D.J.C. (2012). Completeness for two left-sequ ential logics. MSc. thesis Logic, University of Amsterdam (May 2012). https://doi.org/10.48550/arXiv.1206.1936 [cs.LO]. A Proofs - Section 2 Correctness of f . To prove that f :SPA→ FNF is indeed a normalization function we need to prove that for all FEL-terms P , f (P ) terminates, f (P )∈ FNF and EqF...

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1206.1936 2012
[20]

x∧q (y∧q (z∧q F)) = ( x∨q y)∧q (z∧q F)

work page
[21]

¬ x∧q (y∨q T) =¬ (x∧q (y∨q T)) Proof. x∧q (y∧q (z∧q F)) = x∧q ((¬ y∧q z)∧q F) by (FFEL4) and Lemma 2.6.1 = (¬ x∧q ¬ y)∧q (z∧q F) by (FFEL4) and Lemma 2.6.1 =¬ (¬ x∧q ¬ y)∧q (z∧q F) by Lemma 2.6.1 = (x∨q y)∧q (z∧q F), by (FFEL2) 32 ¬ x∧q (y∨q T) =¬ x∨q (y∧q F) by (FFEL10) =¬ (x∧q ¬ (y∧q F)) by (FFEL2) and (FFEL3) =¬ (x∧q ¬ (¬ y∧q ¬ T)) by (FFEL8) and (FFEL...

work page
[22]

m(fa(X[T↦→ F, F↦→ T])) = m(fa(X))[T↦→ F, F↦→ T],

work page
[23]

and by induction La(X1[T ↦→ Y ]) = La(X1)[T ↦→ La(Y )] = La(X)[T ↦→ La(Y )]

f a(X[T↦→ Y, F↦→ Z]) = fa(X)[T↦→ fa(Y ), F↦→ fa(Z)]. Proof. Clause 1 is Lemma 3.3.4 in [6]. We prove clause 2 by induction o n the structure of X. The base cases are trivial. If X = X1 ⊴ b ⊵ X2, distinguish the cases b = a and b̸= a: Case b = a, subcase f = L: La(X[T↦→ Y, F↦→ Z]) = La(X1[T↦→ Y, F↦→ Z]) and by induction, La(X1[T↦→ Y, F↦→ Z]) = La(X1)[T↦→ L...

work page
[24]

˜∧q La(Y )) ⊴ a ⊵ m(Ra(X ′

work page
[25]

= m(X ′ ˜∧q Y )

˜∧q Ra(Y )) by IH and (Aux3) = ... = m(X ′ ˜∧q Y ). (B) m(X ˜∧q Y ) = m(X ˜∧q Y ′). This follows by induction on the depth of X. The base cases X∈{ T, F} are trivial. If X = X1 ⊴ a ⊵ X2 derive m(X ˜∧q Y ) = m((X1 ⊴ a ⊵ X2) ˜∧q Y ) = m(X1[fulland Y ] ⊴ a ⊵ X2[fulland Y ]) = m(La(X1[fulland Y ])) ⊴ a ⊵ m(Ra(X2[fulland Y ])) = m(La(X1)[fulland La(Y )]) ⊴ a ⊵...

work page
[26]

We have to prove that mfe(˜Fβ ∨q (P ∧q Q)) = mfe(˜Fβ ∨q (Q∧q P )), where β∈ As o satisﬁes{β} = α (P ∧q Q)

Let P, Q ∈SP A. We have to prove that mfe(˜Fβ ∨q (P ∧q Q)) = mfe(˜Fβ ∨q (Q∧q P )), where β∈ As o satisﬁes{β} = α (P ∧q Q). By soundness of EqMFEL (Lemma 4.6), it suﬃces to prove that for any β∈ As o that satisﬁes α (P )⊂{ β}, EqMFEL⊢ ˜Fβ ∨q (P ∧q Q) = ˜Fβ ∨q (Q∧q P ). Derive EqMFEL⊢ ˜Fβ ∨q (P ∧q Q) = ( ˜Fβ ∨q (P ∧q F))∨q (P ∧q Q) by Lemma C.2 = ˜Fβ ∨q ((P...

work page
[27]

The soundness of EqC ℓFELU follows as in 1, the additional case is that for any P ∈SP A U\SP A and Q∈SP A U, clfe(P ∧q Q) = clfe(Q∧q P ) = U. 40

work page

[1] [1]

Bergstra, J.A., Bethke, I., and Rodenburg, P.H. (1995). A propositional logic with 4 values: true, false, divergent and meaningless, Journal of Applied Non-Classical Logics , 5(2):199-217. https://doi.org/10.1080/11663081.1995.10510855

work page doi:10.1080/11663081.1995.10510855 1995

[2] [2]

Evaluation trees for proposition algebra

Bergstra, J.A. and Ponse, A. (2015). Evaluation trees fo r proposition algebra. https://doi.org/10.48550/arXiv.1504.08321 [cs.LO]

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1504.08321 2015

[3] [3]

and Ponse, A

Bergstra, J.A. and Ponse, A. (2023). Conditional logic a s a short-circuit logic. https://doi.org/10.48550/arXiv.2304.14821 [cs.LO]

work page doi:10.48550/arxiv.2304.14821 2023

[4] [4]

Short-circuit logic

Bergstra, J.A., Ponse, A., and Staudt, D.J.C. (2010 / 201 3). Short-circuit logic. (First version appeared in 2010.) https://doi.org/10.48550/arXiv.1010.3674 [cs.LO,math.LO]

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1010.3674 2010

[5] [5]

Bergstra, J.A., Ponse, A., and Staudt, D.J.C. (2018). Pr opositional logic with short-circuit evaluation: a non-commutative and a commutative variant. https://doi.org/10.48550/arXiv.1810.02142 [cs.LO,math.LO]

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1810.02142 2018

[6] [6]

Bergstra, J.A., Ponse, A., and Staudt, D.J.C. (2021). No n-commutative propositional logic with short- circuit evaluation. Journal of Applied Non-Classical Logics , 31(3-4):234-278 (online available). https://doi.org/10.1080/11663081.2021.2010954

work page doi:10.1080/11663081.2021.2010954 2021

[7] [7]

Blok, A. (2011). Side-Eﬀecting Logic, [Unpublished manuscript], University of Amsterdam

work page 2011

[8] [8]

Bochvar, D.A. (1938). On a 3-valued logical calculus and its application to the analysis of contradictions (in Russian). Matematicheskii Sbornik, 4(2):287-308

work page 1938

[9] [9]

Contractive SCL

Burris, S.N. and Sankappanavar, H.P. (2012). A Course in Universal Algebra - The Millennium Edition . Available at http://www.math.uwaterloo.ca/~snburris/htdocs/ualg.html. 6Suppose A = {a}. Then there are 5 ·44 ·33 terms composed of four elements of {a,¬ a, a ∨q T, a ∧q F} and the three connectives in { ∧q , ∨q , ↔← } that have evaluation trees of depth 4...

work page 2012

[10] [10]

Church, A. (1956). Introduction to Mathematical Logic . Princeton University Press

work page 1956

[11] [11]

Cornets de Groot, S.H. (2012). Logical systems with lef t-sequential versions of NAND and XOR. MSc. thesis Logic, University of Amsterdam (June 2020). https://eprints.illc.uva.nl/id/eprint/1743/1/MoL-2020-02.text.pdf

work page 2012

[12] [12]

and Squier, C.C

Guzm´ an, F. and Squier, C.C. (1990). The algebra of cond itional logic. Algebra Universalis , 27:88-110. https://doi.org/10.1007/BF01190256

work page doi:10.1007/bf01190256 1990

[13] [13]

Hoare, C.A.R. (1985). A couple of novelties in the propo sitional calculus. Zeitschrift f¨ ur Mathematische Logik und Grundlagen der Mathematik , 31(2):173-178. https://doi.org/10.1002/malq.19850310905

work page doi:10.1002/malq.19850310905 1985

[14] [14]

Kleene, S.C. (1938). On a notation for ordinal numbers. Journal of Symbolic Logic , 3:150-155

work page 1938

[15] [15]

McCarthy, J. (1963). A basis for a mathematical theory o f computation. In P. Braﬀort and D. Hirschberg (eds.), Computer Programming and Formal Systems , pages 33–70, North-Holland, Amsterdam

work page 1963

[16] [16]

McCune W. (2008). The GUI: Prover9 and Mace4 with a graph ical user interface. Prover9-Mace4 Version 0.5B. (Prover9-Mace4-v05B.zip, March 14, 2008). https://www.cs.unm.edu/~mccune/prover9/gui/v05.html

work page 2008

[17] [17]

and Ponse, A

Papuc, D. and Ponse, A. (2022). Non-commutative propos itional logic with short-circuited biconditional and NAND. https://doi.org/10.48550/arXiv.2203.09321 [cs.LO]

work page doi:10.48550/arxiv.2203.09321 2022

[18] [18]

and Staudt, D.J.C

Ponse, A. and Staudt, D.J.C. (2018). An independent axi omatisation for free short-circuit logic. Journal of Applied Non-Classical Logics , 28(1), 35-71 (online available). https://doi.org/10.1080/11663081.2018.1448637

work page doi:10.1080/11663081.2018.1448637 2018

[19] [19]

Staudt, D.J.C. (2012). Completeness for two left-sequ ential logics. MSc. thesis Logic, University of Amsterdam (May 2012). https://doi.org/10.48550/arXiv.1206.1936 [cs.LO]. A Proofs - Section 2 Correctness of f . To prove that f :SPA→ FNF is indeed a normalization function we need to prove that for all FEL-terms P , f (P ) terminates, f (P )∈ FNF and EqF...

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1206.1936 2012

[20] [20]

x∧q (y∧q (z∧q F)) = ( x∨q y)∧q (z∧q F)

work page

[21] [21]

¬ x∧q (y∨q T) =¬ (x∧q (y∨q T)) Proof. x∧q (y∧q (z∧q F)) = x∧q ((¬ y∧q z)∧q F) by (FFEL4) and Lemma 2.6.1 = (¬ x∧q ¬ y)∧q (z∧q F) by (FFEL4) and Lemma 2.6.1 =¬ (¬ x∧q ¬ y)∧q (z∧q F) by Lemma 2.6.1 = (x∨q y)∧q (z∧q F), by (FFEL2) 32 ¬ x∧q (y∨q T) =¬ x∨q (y∧q F) by (FFEL10) =¬ (x∧q ¬ (y∧q F)) by (FFEL2) and (FFEL3) =¬ (x∧q ¬ (¬ y∧q ¬ T)) by (FFEL8) and (FFEL...

work page

[22] [22]

m(fa(X[T↦→ F, F↦→ T])) = m(fa(X))[T↦→ F, F↦→ T],

work page

[23] [23]

and by induction La(X1[T ↦→ Y ]) = La(X1)[T ↦→ La(Y )] = La(X)[T ↦→ La(Y )]

f a(X[T↦→ Y, F↦→ Z]) = fa(X)[T↦→ fa(Y ), F↦→ fa(Z)]. Proof. Clause 1 is Lemma 3.3.4 in [6]. We prove clause 2 by induction o n the structure of X. The base cases are trivial. If X = X1 ⊴ b ⊵ X2, distinguish the cases b = a and b̸= a: Case b = a, subcase f = L: La(X[T↦→ Y, F↦→ Z]) = La(X1[T↦→ Y, F↦→ Z]) and by induction, La(X1[T↦→ Y, F↦→ Z]) = La(X1)[T↦→ L...

work page

[24] [24]

˜∧q La(Y )) ⊴ a ⊵ m(Ra(X ′

work page

[25] [25]

= m(X ′ ˜∧q Y )

˜∧q Ra(Y )) by IH and (Aux3) = ... = m(X ′ ˜∧q Y ). (B) m(X ˜∧q Y ) = m(X ˜∧q Y ′). This follows by induction on the depth of X. The base cases X∈{ T, F} are trivial. If X = X1 ⊴ a ⊵ X2 derive m(X ˜∧q Y ) = m((X1 ⊴ a ⊵ X2) ˜∧q Y ) = m(X1[fulland Y ] ⊴ a ⊵ X2[fulland Y ]) = m(La(X1[fulland Y ])) ⊴ a ⊵ m(Ra(X2[fulland Y ])) = m(La(X1)[fulland La(Y )]) ⊴ a ⊵...

work page

[26] [26]

We have to prove that mfe(˜Fβ ∨q (P ∧q Q)) = mfe(˜Fβ ∨q (Q∧q P )), where β∈ As o satisﬁes{β} = α (P ∧q Q)

Let P, Q ∈SP A. We have to prove that mfe(˜Fβ ∨q (P ∧q Q)) = mfe(˜Fβ ∨q (Q∧q P )), where β∈ As o satisﬁes{β} = α (P ∧q Q). By soundness of EqMFEL (Lemma 4.6), it suﬃces to prove that for any β∈ As o that satisﬁes α (P )⊂{ β}, EqMFEL⊢ ˜Fβ ∨q (P ∧q Q) = ˜Fβ ∨q (Q∧q P ). Derive EqMFEL⊢ ˜Fβ ∨q (P ∧q Q) = ( ˜Fβ ∨q (P ∧q F))∨q (P ∧q Q) by Lemma C.2 = ˜Fβ ∨q ((P...

work page

[27] [27]

The soundness of EqC ℓFELU follows as in 1, the additional case is that for any P ∈SP A U\SP A and Q∈SP A U, clfe(P ∧q Q) = clfe(Q∧q P ) = U. 40

work page