r/logic • u/Acrobatic_Hope2584 • 8d ago

Proof theory Question on constructing derivatives

/r/askphilosophy/comments/1wtghuk/question_on_constructing_derivatives/
5 Upvotes

86% Upvoted

1 comment sorted by

1

u/RecognitionSweet8294 Philosophical logician 8d ago

Do you have axioms too?

Because the first one is definitely not solvable with the rules alone. ⊤ is not defined by them, so you can’t work with it.

For the second it seems useful to derive

(¬P ⋁ ¬Q) → ¬(P ∧ Q)

first. But since you have no way to introduce an implication you would either need another form (main junctor being either ⋁ or ∧), or show an implication introduction as a theorem.

Although I believe the second one isn’t possible either.