Closed Jean-Luc-Picard-2021 closed 3 months ago
Ok, I can generate the same proof in Fitch style, if I replace in the output generator this here:
Variant 1:
rewrite_term(V, J, K, V) :- var(V), !,
rewrite_name(J, V), K is J+1.
By this here:
Variant 2:
rewrite_term(V, J, J, V) :- var(V), !,
rewrite_name(J, V).
These are the two proofs:
Variant 1:
Variant 2:
I think both are valid. But it still scares the shit out of me, that this aliasing still gives a valid proof.
I am not 100% sure, but this proof looks wrong:
∀x∀y p(x,y) → ∃x ∃y p(x,y) https://www.umsu.de/trees/#~6x~6yp(x,y)~5~7x~7yp(x,y)
Shouldn't the ∀ rule generate a totally new parameter? In case it is a δ-rule, like here:
First-Order Modal Tableaux https://www.academia.edu/4038862/First_Order_Modal_Tableaux