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.