eyeprolog

Intuitionistic logic with a Kripke model

When is “p or not p” not automatically true?

In classical logic every statement is true or false. In intuitionistic logic a statement is true only once there is evidence for it, and evidence can grow over time. This example builds a small Kripke model, a finite picture of growing knowledge, and shows that excluded middle, “p or not p”, need not hold.

Run it in the playground · Source

The question

Start with no information at a root world. Later, you may learn p (the left world) or q (the right world), and eventually both. Which formulas are already established at the root, and which are not?

The model

step(root, left).
step(root, right).
step(left, both).
step(right, both).

base(left, p).
base(right, q).

leq(World, World) :- world(World).
leq(From, To) :- step(From, Mid), leq(Mid, To).

step/2 says how knowledge can grow, and leq/2 is its reflexive, transitive closure: “To is a possible future of From”. At left we learn p, at right we learn q.

The rules

forces(World, atom(Prop)) :-
  leq(Someworld, World),
  base(Someworld, Prop).

forces(World, implies(Left, Right)) :-
  world(World),
  \+ bad_implication(World, Left, Right).

bad_implication(World, Left, Right) :-
  leq(World, Future),
  forces(Future, Left),
  \+ forces(Future, Right).

A world forces an atom once the atom was learned there or earlier, so knowledge persists. An implication holds when no future world has its premise without its conclusion. neg(F) is “F implies bottom”, and or needs one side established now.

The answer

eyeprolog examples/intuitionistic-logic-kripke.pl

intuitionistic_truth(monotone_p_reaches_both, both, atom(p)).
intuitionistic_truth(constructive_case_analysis, root, implies(atom(p), or(atom(p), atom(q)))).
intuitionistic_truth(double_negated_branch_information, root, neg(neg(or(atom(p), atom(q))))).
intuitionistic_countermodel(root_does_not_decide_branch, root, or(atom(p), atom(q))).
intuitionistic_countermodel(excluded_middle_not_forced, root, or(atom(p), neg(atom(p)))).

At the root, “p or q” is not yet established, and neither is “p or not p”: p is unknown, yet it is not refuted either, because a future world learns it. Still, “not not (p or q)” holds: it can never be refuted.

The reason

eyeprolog --proof examples/intuitionistic-logic-kripke.pl

step(intuitionistic_countermodel(excluded_middle_not_forced, root, or(atom(p), neg(atom(p)))),
     rule(24),
     [],
     [\+ forces(root, or(atom(p), neg(atom(p))))]).
step(\+ forces(root, or(atom(p), neg(atom(p)))), absent, [], []).

The countermodel claim rests on a failed search: no derivation of “p or not p” at the root exists. Its step is marked absent, a completed negation that a checker cannot replay as a clause.

The check

condition('C1', resolution, ok, 15).
condition('C6', boundary_consistency, ok, 0).
obligation(absent, theory_scoped, \+ forces(root, or(atom(p), neg(atom(p))))).
verdict(checked_with_obligations).

All 15 rule and fact steps replay. The four negations, two \+ forces and two \+ bad_implication, are obligations: the checker records that the result depends on these searches having found nothing, and leaves them as trusted boundaries rather than claiming to have proved them.

Try it

Add base(root, p). so p is known from the start. Both countermodel answers disappear: with p at the root, “p or not p” and “p or q” hold.
Add a world where p is learned later than left and predict which answers change.
Check whether implies(neg(neg(atom(p))), atom(p)) (double-negation elimination) is forced at the root.

Learn more in The Art of EyeProlog, Chapter 7.

This site is open source. Improve this page.