%%% pauline.pl -- normalized inference over the Pauline corpus %%% %%% Negation is EXPLICIT (neg/1), never negation-as-failure. Paul argues %%% classically: the corpus is full of modus tollens and contrapositive %%% stacks, and NAF cannot express either. The price is that we need our %%% own prover instead of riding SLD resolution. The payoff is 1 Cor 1, %%% at the bottom, where Paul refuses NAF out loud. %%% %%% run: swipl pauline.pl :- discontiguous fact/2. :- discontiguous imp/3. :- discontiguous ord/3. %%%=========================================================== %%% THE KNOWLEDGE BASE %%%=========================================================== %%% --- 1 Cor 6:2-3 ------------------------------------------- %%% "Do ye not know that the saints shall judge the world?" %%% ouk oidate: not a premise. An audit. Paul never argues for these, %%% he asserts the reader already holds them and isn't querying. fact(judges(saints, world), '1Cor 6:2 ouk oidate'). fact(member(you, saints), '1Cor 6:2'). fact(judges(saints, angels), '1Cor 6:3 ouk oidate'). %%% posoi mallon / "how much more" -- the a fortiori ordering. %%% This is the premise Paul never states and the whole argument needs. ord(world, smallest_matters, '1Cor 6:2 qal vahomer'). ord(angels, this_life, '1Cor 6:3 posoi mallon'). %%% --- 1 Cor 15:13-20 ---------------------------------------- %%% Seven verses of pure negative propagation, discharged by one %%% positive assertion at v20. The best contrapositive stack in the NT. imp(neg(resurrection_of_dead), neg(risen(christ)), '1Cor 15:13'). imp(neg(risen(christ)), vain(preaching), '1Cor 15:14'). imp(neg(risen(christ)), vain(faith), '1Cor 15:14'). imp(neg(risen(christ)), false_witness(apostles), '1Cor 15:15'). imp(neg(risen(christ)), still_in_sins(you), '1Cor 15:17'). fact(risen(christ), '1Cor 15:20 nuni de -- "But now is Christ risen"'). %%% --- Rom 8:38-39 ------------------------------------------- %%% Paul writes a negated disjunction. Normalizing it is a literal %%% De Morgan expansion into a conjunction of negations. %%% Note the shape: paired extremes along axes, not a flat list. %%% Naming both poles of a dimension implies everything between. neg_or([ separates(death, us, love_of_god), % biological separates(life, us, love_of_god), separates(angels, us, love_of_god), % hierarchical separates(principalities, us, love_of_god), separates(powers, us, love_of_god), separates(things_present, us, love_of_god), % temporal separates(things_to_come, us, love_of_god), separates(height, us, love_of_god), % spatial separates(depth, us, love_of_god) ], 'Rom 8:38-39'). %%% "nor any other creature" (ktisis hetera) is a DOMAIN CLOSURE AXIOM. %%% It does not extend the list -- it changes the TYPE of the claim, %%% from a finite conjunction to a quantifier bounded by a sort. %%% %%% This one clause carries the entire Creator/creature partition, and %%% it is the only thing standing between the argument and an infinite %%% regress of "but what about--". Get it wrong and the prover keeps %%% emitting confident conclusions with a real verse number attached. creature(X) :- nonvar(X), \+ uncreated(X). uncreated(god). uncreated(love_of_god). %%% --- Gal 3:28 ---------------------------------------------- %%% Looks like Rom 8:38 but isn't. Not neg(A or B) over a fixed domain -- %%% the predicate stops being a valid discriminator. Dropping an index, %%% not negating a row. irrelevant_sort(jew, 'Gal 3:28'). irrelevant_sort(greek, 'Gal 3:28'). irrelevant_sort(bond,'Gal 3:28'). irrelevant_sort(free, 'Gal 3:28'). irrelevant_sort(male,'Gal 3:28'). irrelevant_sort(female, 'Gal 3:28'). %%% --- Rom 6:1-2 --------------------------------------------- %%% me genoito. Paul's answer to "shall we sin more?" is not `false`. %%% It is POS -- *how*. dead_to(we,sin) removes `we` from the domain %%% lives_in(_,sin) ranges over. A sort violation, not a falsehood: %%% Prolog wouldn't return false, it would fail to unify. fact(dead_to(we, sin), 'Rom 6:2'). sort_violation(lives_in(X,Y), dead_to(X,Y), 'Rom 6:2 pos eti zesomen'). %%% --- 1 Cor 1:14-16 -- THE CONTROL CASE --------------------- %%% The same move, unhardened. Paul enumerates, patches the list %%% mid-sentence, and then declines to close it: %%% %%% "I baptized none of you, but Crispus and Gaius ... %%% And I baptized also the household of Stephanas: %%% BESIDES, I KNOW NOT WHETHER I baptized any other." %%% %%% No closure axiom. He states the gap out loud. This is Paul under %%% live fire on a topic he hasn't rehearsed -- and it is the proof %%% that Rom 8:39 is deliberate rather than decorative. baptized_list([crispus, gaius, household_of_stephanas], '1Cor 1:14-16'). %%%=========================================================== %%% THE PROVER %%%=========================================================== %%% Iterative deepening -> shortest proof first, and it terminates %%% despite the DNI/DNE pair being mutually recursive. prove(P, Proof) :- between(1, 8, D), prove(P, Proof, D), !. % axioms prove(P, axiom(P,C), _) :- fact(P, C). % enumerated, unclosed (1 Cor 1) prove(baptized(paul,X), axiom(baptized(paul,X),C), _) :- baptized_list(L, C), memberchk(X, L). % modus ponens prove(P, mp(C,S), D) :- D > 0, D1 is D-1, imp(A, P, C), prove(A, S, D1). % modus tollens -- the workhorse. me genoito is always the neg(Q). prove(neg(A), mt(C,S), D) :- D > 0, D1 is D-1, imp(A, Q, C), prove(neg(Q), S, D1). % De Morgan: neg over a disjunction distributes prove(neg(P), demorgan(C), _) :- neg_or(L, C), memberchk(P, L). % domain closure: "nor any other creature" prove(neg(separates(X,us,love_of_god)), closure('Rom 8:39 ktisis hetera'), _) :- creature(X), \+ (neg_or(L,_), memberchk(separates(X,us,love_of_god), L)). % sort violation (Rom 6:2) -- unsatisfiable, not false prove(neg(P), sort_error(C,S), D) :- D > 0, D1 is D-1, sort_violation(P, Guard, C), prove(Guard, S, D1). % dropped discriminator (Gal 3:28) prove(neg(discriminates(S)), sort_dropped(C), _) :- irrelevant_sort(S, C). % universal instantiation over group membership prove(G, ui(S1,S2), D) :- D > 0, D1 is D-1, G =.. [F,X,Y], F \== neg, F \== member, atom(X), GG =.. [F,Grp,Y], prove(GG, S1, D1), prove(member(X,Grp), S2, D1). % a fortiori -- qal vahomer / polloi mallon prove(G, afortiori(C,S), D) :- D > 0, D1 is D-1, G =.. [F,X,Lesser], F \== neg, ord(Greater, Lesser, C), GG =.. [F,X,Greater], prove(GG, S, D1). % double negation, introduction then elimination (DNE last: expensive) prove(neg(neg(P)), dni(S), D) :- D > 0, D1 is D-1, prove(P, S, D1). prove(P, dne(S), D) :- D > 0, D1 is D-1, P \= neg(_), prove(neg(neg(P)), S, D1). %%% What negation-as-failure WOULD conclude. Nothing above uses this. %%% 1 Cor 1:16 is Paul explicitly declining to run it. naf_says(neg(baptized(paul,X))) :- \+ (baptized_list(L,_), memberchk(X, L)). %%%=========================================================== %%% PRETTY PRINTING %%%=========================================================== show(P) :- format("~n~w~w~n", ['?- ', P]), ( prove(P, Proof) -> pp(Proof, 2) ; format(" NOT DERIVABLE~n") ). pp(axiom(P,C), I) :- tab(I), format("~w~t~35| [~w]~n", [P,C]). pp(demorgan(C), I) :- tab(I), format("de Morgan~t~35| [~w]~n", [C]). pp(closure(C), I) :- tab(I), format("domain closure~t~35| [~w]~n", [C]). pp(sort_dropped(C), I) :- tab(I), format("sort dropped~t~35| [~w]~n", [C]). pp(mp(C,S), I) :- tab(I), format("modus ponens~t~35| [~w]~n",[C]), step(S,I). pp(mt(C,S), I) :- tab(I), format("modus tollens~t~35| [~w]~n",[C]), step(S,I). pp(afortiori(C,S), I) :- tab(I), format("a fortiori~t~35| [~w]~n",[C]), step(S,I). pp(sort_error(C,S), I) :- tab(I), format("sort violation~t~35| [~w]~n",[C]), step(S,I). pp(dni(S), I) :- tab(I), format("double-neg intro~n"), step(S,I). pp(dne(S), I) :- tab(I), format("double-neg elim~n"), step(S,I). pp(ui(S1,S2), I) :- tab(I), format("universal instantiation~n"), step(S1,I), step(S2,I). step(S,I) :- I1 is I+3, pp(S,I1). %%%=========================================================== %%% WHERE THIS BREAKS: 1 Cor 7 is non-monotonic %%%=========================================================== %%% Paul tags clauses with provenance and defeasibility INLINE: %%% 7:6 "by permission, and not of commandment" %%% 7:12 "to the rest speak I, not the Lord" %%% 7:25 "I have no commandment of the Lord: yet I give my judgment" %%% These are defaults with exceptions. Horn clauses won't hold them and %%% the prover above has no way to rank them -- you'd need defeasible %%% logic with a priority order over rules. Recorded, not used: provenance('1Cor 7:10', commandment_of_lord). provenance('1Cor 7:12', paul_not_lord). provenance('1Cor 7:25', judgment_of_paul). %%%=========================================================== main :- format("~n=== 1 Cor 6: instantiation, then a fortiori ==="), show(judges(you, world)), show(judges(you, smallest_matters)), show(judges(you, this_life)), format("~n~n=== 1 Cor 15: the contrapositive stack ==="), show(resurrection_of_dead), format("~n~n=== Rom 8:38-39: De Morgan, then closure ==="), show(neg(separates(principalities, us, love_of_god))), show(neg(separates(quantum_decoherence, us, love_of_god))), show(neg(separates(god, us, love_of_god))), format("~n~n=== Rom 6:2 / Gal 3:28: sort, not truth-value ==="), show(neg(lives_in(we, sin))), show(neg(discriminates(greek))), format("~n~n=== 1 Cor 1:14-16: the control case, left open ==="), show(baptized(paul, crispus)), show(neg(baptized(paul, fortunatus))), format("~n negation-as-failure would say: "), ( naf_says(neg(baptized(paul, fortunatus))) -> format("YES, Paul did not baptize him.~n"), format(" 1 Cor 1:16 declines to run it. He says he cannot recall.~n") ; format("nothing.~n") ), format("~n~n=== not a yes-machine ==="), show(vain(faith)), show(judges(you, god)), nl. :- initialization(main, main).