Message Boards Message Boards

How to input ((∃x : a • p) ∧ (∀x : a • p ⇒ q)) ⇒ (∃x : a • q)?

GROUPS:

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.

POSTED BY: Daniel Wilkinson
Answer
2 months ago

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.

POSTED BY: Sean Clarke
Answer
2 months ago

Thanks, I'm downloading Mathematica now and will give that a shot.

POSTED BY: Daniel Wilkinson
Answer
2 months ago

Group Abstract Group Abstract