Lean verification registry · Authored proofs · The Logos Architecture
Written formal sequents verified
Axiom-free: true · 1 checked theorem statements.
Lean establishes the listed formal statements and dependencies. The exact authored source, Ground, known premise meanings, application validation and empirical evidence remain separately typed. No unencoded section is certified by a neighboring theorem.
Original source author: Maclain Hunter. Machine formalization: Replit Agent. No original wording was rewritten.
Source registered: 2026-10-02T15:32:29.681Z (not original authorship).
Formalized: 2026-10-03T10:37:05.082Z.
Checked: 2026-10-03T10:41:55.398Z.
Independent timestamp: 2026-10-03T10:42:55.000Z.
Authored source SHA-256: 6b440525a80e6efd2ba6d948fe46ecc50df305a92b5d7f8c5cc7d2e5a54cb068
Lean source · Verification JSON · Exact archived source JSON · Compiler report · Current authored source page · Signed release and verification instructions
Lean (version 4.7.0, commit v4.7.0, Release) exitCode=0 'HunterAuthored.inference_1' does not depend on any axioms
{P, P <-> Q, Q <-> R, R <-> S, S <-> T, T <-> U} |= (((P & Q) & (R & S)) & T) & U
Exact source sequent under finite two-valued propositional semantics. Source proposition meanings and Logic/Logos/God Ground are preserved separately; this checks the inference, not unencoded prose.
The Appearance of a Paradox by Maclain Hunter:
Abstract: I will demonstrate that Russell’s Liar’s Paradox is merely the result of a failure to apply proper order of operations in the logical reasoning with self-referential statements.
Premises:
P: A semantically empty statement like that found in the Liar’s Paradox where S represents a statement like “statement S is false” is not a valid statement, negating the relevance of the output of reasoning and operations performed with or on the statement. This is because using the empty statement as the referent for its own truth value is an absurdity.
Q: Trying to find the truth value of a statement like S amounts to saying “nothing is true” and/or “nothing is false”.
R: Among other logical issues with the statement in the Liar’s Paradox, premise Q helps us to see that the statement S is logically equivalent to a fallacious generalization that swings between negation of Truth and the negation of falseness, which is a logically untenable position (as Truth is inherent to Reality).
S: A statement like S being invalid doesn’t reflect a limitation in Logic but rather in the statement. The fact Logic can help us understand there is something odd and wrong about a statement like S in the first place is a display of its purpose/practice.
T: Propositions must meet basic semantic and syntactic requirements, namely the logical rules including Identity, Non-Contradiction, the Excluded Middle, the Principle of Sufficient Reason, De Morgan’s Law, Modus Ponens, and Modus Tollens. Propositions that don’t conform to logical rules do not qualify for the next stages of reasoning that would be entailed by having prepared a valid proposition.
U: Assume ~{P, Q, R, S, T}. This leads to logical contradiction, most famously in the form of the Liar’s Paradox. Ergo a valid resolution to the famous (alleged) paradox is the acceptance of the Truth of the premises.
Proof:
{P, P <-> Q, Q <-> R, R <-> S, S <-> T, T <-> U} |= (((P & Q) & (R & S)) & T) & U
Conclusion: There is no Liar’s Paradox, just poor reasoning that led people to believe it. Proper logical order of operations shows that, how, and why the statement S cannot pass muster to even be reasoned with as a valid proposition. To try to reason with it (S) is incoherent and wrong-headed - unless one understands it can’t be a valid statement and that it is merely an exercise to explore logical systems. The paradox is an illusion and logically consistent Logic (with proper order of operations) necessarily functions perfectly.
Analogy:
An analogy, for what the Liar’s Paradox is essentially doing logically, is putting water instead of gas in the gas tank of a car, then declaring engines have flaws and limitations due to the fact your car predictably/properly won’t/wouldn’t start. It’s not a legitimate complaint about the machinery and mechanics. Put gas in the gas tank (and valid statements into Logical Systems) - paradox and problem solved (with common sense frankly).
Truth Table Analysis:
valid
↓ ↓ ↓ ↓ ↓ ↓ ↓
PQRSTU⎪P P↔Q Q↔R R↔S S↔T T↔U╞(((P&Q)&(R&S))&T)&U
―――――――――――――――――――――――――――――――――――――――――――――――――
TTTTTT⎪T TTT TTT TTT TTT TTT TTT T TTT TT TT
TTTTTF⎪T TTT TTT TTT TTT TFF TTT T TTT TT FF
TTTTFT⎪T TTT TTT TTT TFF FFT TTT T TTT FF FT
TTTTFF⎪T TTT TTT TTT TFF FTF TTT T TTT FF FF
TTTFTT⎪T TTT TTT TFF FFT TTT TTT F TFF FT FT
TTTFTF⎪T TTT TTT TFF FFT TFF TTT F TFF FT FF
TTTFFT⎪T TTT TTT TFF FTF FFT TTT F TFF FF FT
TTTFFF⎪T TTT TTT TFF FTF FTF TTT F TFF FF FF
TTFTTT⎪T TTT TFF FFT TTT TTT TTT F FFT FT FT
TTFTTF⎪T TTT TFF FFT TTT TFF TTT F FFT FT FF
TTFTFT⎪T TTT TFF FFT TFF FFT TTT F FFT FF FT
TTFTFF⎪T TTT TFF FFT TFF FTF TTT F FFT FF FF
TTFFTT⎪T TTT TFF FTF FFT TTT TTT F FFF FT FT
TTFFTF⎪T TTT TFF FTF FFT TFF TTT F FFF FT FF
TTFFFT⎪T TTT TFF FTF FTF FFT TTT F FFF FF FT
TTFFFF⎪T TTT TFF FTF FTF FTF TTT F FFF FF FF
TFTTTT⎪T TFF FFT TTT TTT TTT TFF F TTT FT FT
TFTTTF⎪T TFF FFT TTT TTT TFF TFF F TTT FT FF
TFTTFT⎪T TFF FFT TTT TFF FFT TFF F TTT FF FT
TFTTFF⎪T TFF FFT TTT TFF FTF TFF F TTT FF FF
TFTFTT⎪T TFF FFT TFF FFT TTT TFF F TFF FT FT
TFTFTF⎪T TFF FFT TFF FFT TFF TFF F TFF FT FF
TFTFFT⎪T TFF FFT TFF FTF FFT TFF F TFF FF FT
TFTFFF⎪T TFF FFT TFF FTF FTF TFF F TFF FF FF
TFFTTT⎪T TFF FTF FFT TTT TTT TFF F FFT FT FT
TFFTTF⎪T TFF FTF FFT TTT TFF TFF F FFT FT FF
TFFTFT⎪T TFF FTF FFT TFF FFT TFF F FFT FF FT
TFFTFF⎪T TFF FTF FFT TFF FTF TFF F FFT FF FF
TFFFTT⎪T TFF FTF FTF FFT TTT TFF F FFF FT FT
TFFFTF⎪T TFF FTF FTF FFT TFF TFF F FFF FT FF
TFFFFT⎪T TFF FTF FTF FTF FFT TFF F FFF FF FT
TFFFFF⎪T TFF FTF FTF FTF FTF TFF F FFF FF FF
FTTTTT⎪F FFT TTT TTT TTT TTT FFT F TTT FT FT
FTTTTF⎪F FFT TTT TTT TTT TFF FFT F TTT FT FF
FTTTFT⎪F FFT TTT TTT TFF FFT FFT F TTT FF FT
FTTTFF⎪F FFT TTT TTT TFF FTF FFT F TTT FF FF
FTTFTT⎪F FFT TTT TFF FFT TTT FFT F TFF FT FT
FTTFTF⎪F FFT TTT TFF FFT TFF FFT F TFF FT FF
FTTFFT⎪F FFT TTT TFF FTF FFT FFT F TFF FF FT
FTTFFF⎪F FFT TTT TFF FTF FTF FFT F TFF FF FF
FTFTTT⎪F FFT TFF FFT TTT TTT FFT F FFT FT FT
FTFTTF⎪F FFT TFF FFT TTT TFF FFT F FFT FT FF
FTFTFT⎪F FFT TFF FFT TFF FFT FFT F FFT FF FT
FTFTFF⎪F FFT TFF FFT TFF FTF FFT F FFT FF FF
FTFFTT⎪F FFT TFF FTF FFT TTT FFT F FFF FT FT
FTFFTF⎪F FFT TFF FTF FFT TFF FFT F FFF FT FF
FTFFFT⎪F FFT TFF FTF FTF FFT FFT F FFF FF FT
FTFFFF⎪F FFT TFF FTF FTF FTF FFT F FFF FF FF
FFTTTT⎪F FTF FFT TTT TTT TTT FFF F TTT FT FT
FFTTTF⎪F FTF FFT TTT TTT TFF FFF F TTT FT FF
FFTTFT⎪F FTF FFT TTT TFF FFT FFF F TTT FF FT
FFTTFF⎪F FTF FFT TTT TFF FTF FFF F TTT FF FF
FFTFTT⎪F FTF FFT TFF FFT TTT FFF F TFF FT FT
FFTFTF⎪F FTF FFT TFF FFT TFF FFF F TFF FT FF
FFTFFT⎪F FTF FFT TFF FTF FFT FFF F TFF FF FT
FFTFFF⎪F FTF FFT TFF FTF FTF FFF F TFF FF FF
FFFTTT⎪F FTF FTF FFT TTT TTT FFF F FFT FT FT
FFFTTF⎪F FTF FTF FFT TTT TFF FFF F FFT FT FF
FFFTFT⎪F FTF FTF FFT TFF FFT FFF F FFT FF FT
FFFTFF⎪F FTF FTF FFT TFF FTF FFF F FFT FF FF
FFFFTT⎪F FTF FTF FTF FFT TTT FFF F FFF FT FT
FFFFTF⎪F FTF FTF FTF FFT TFF FFF F FFF FT FF
FFFFFT⎪F FTF FTF FTF FTF FFT FFF F FFF FF FT
FFFFFF⎪F FTF FTF FTF FTF FTF FFF F FFF FF FF
Q.E.D.