So far, the assistant automatically checks only derivation of new assumptions from existing ones, but can neither derive admissible assumptions from goals (goal: φ → ψ / assumption: φ), nor detect that proving a sub-goal suffices to prove a super-goal (goal: φ → ψ / goal: ψ). Goals are treated specially and on a very basic level.
Goals can be made essentially “first-class” citizens by treating them similarly to F-formulas in tableaux. This requires adjustments to proof structure, validation, and rules (matchers).
Rules (matchers) have to operate not only assumptions, but, also on goals and combinations of assumptions and goals.
Validation needs to collect not only sets of assumptions, but also sets of active goals. Each branch is thus a sequent.
Proof structure should probably have five kinds of nodes:
Axiom
No proof.
One child; when collecting a sequent for its validation, the axiom's formula is an assumption.
Should only appear at the top level of a theory.
A regular assumption
Proved by a rule (matcher) from the sequent collected along the path to it.
One child; when collecting a sequent for its validation, the regular assumptions's formula is an assumption.
Claim/Lemma/Theorem
Has a proof. The claim's formula is treated as a goal in this proof.
It has one child starting the subsequent proof. When collecting a sequent for its validation, the claim's formula is an assumption.
“Suffices to prove” goal
Has a proof. The goal's formula is treated as a goal in this proof.
No children, but some existing goal must be derivable by some rule when this goal's formula is taken as an assumption.
Case-analysis
No proof.
Two (or more) children, all can be derived by a split (β) rule from a single assumption or goal. Children can be assumptions or goals (depending on the formula). It'd be nice to allow more children for n-ary assumed disjunctions/goal conjunctions.
A goal is proved if all branches of its proof are closed.
A branch is closed if the sequent collected in its leaf either has:
some formula φ as both a goal and an assumption, or
two assumptions: φ and ¬φ (contradiction), or
two goals: φ and ¬φ, or
explicit falsity as assumption, or
explicit truth as goal.
Note that this treatment will essentially eliminate the need for proof by contradiction (it is derivable by a rule that when proving a goal φ, you can assume ¬φ, and vice versa), and proof by generalization (just a special case of “Suffices to prove” goal).
So far, the assistant automatically checks only derivation of new assumptions from existing ones, but can neither derive admissible assumptions from goals (goal: φ → ψ / assumption: φ), nor detect that proving a sub-goal suffices to prove a super-goal (goal: φ → ψ / goal: ψ). Goals are treated specially and on a very basic level.
Goals can be made essentially “first-class” citizens by treating them similarly to F-formulas in tableaux. This requires adjustments to proof structure, validation, and rules (matchers).
Rules (matchers) have to operate not only assumptions, but, also on goals and combinations of assumptions and goals.
Validation needs to collect not only sets of assumptions, but also sets of active goals. Each branch is thus a sequent.
Proof structure should probably have five kinds of nodes:
A goal is proved if all branches of its proof are closed.
A branch is closed if the sequent collected in its leaf either has:
Note that this treatment will essentially eliminate the need for proof by contradiction (it is derivable by a rule that when proving a goal φ, you can assume ¬φ, and vice versa), and proof by generalization (just a special case of “Suffices to prove” goal).