I would like to input the statement ((∃x : a • p) ∧ (∀x : a • p ⇒ q)) ⇒ (∃x : a • q) in order to generate a proof tree using both introduction and elimination rules.
Is Wolfram able to do this? When I input the statement currently, it says it does not fully understand.
For longer, more involved things like this, you would want to use Mathematica or Mathematica online.
I don't think there's a built in function for generating such readable proof trees. Maybe there's a package out there for it. Are you using Sequent Calculus? Which formal logic exactly did you want to use? I would look online to see anyone had made a tool for working with them in Mathematica.
Thanks, I'm downloading Mathematica now and will give that a shot.