A3 Q3 Formal Proof

[Henry S]

Hi,

1. For assignment 3 question 3 that asks you to do a formal proof, are
we allowed to substitute ∧ (and) with -> (implies) and ¬ (not)?

For example, if we are asked to show |- p ∧ q, can we show |- ¬(p-> ¬q)
since the 2 formulas are equivalent?

2. Also, in using Axiom 1-9, can we substitute ◻A for any WFF?
For example, Ax1 is: A->(B->A), so can we write ◻A->(◻B->◻A) as an
application of Ax1?


Thanks,
Henry

[Curtis Bright]

Post by Henry S
1. For assignment 3 question 3 that asks you to do a formal proof, are
we allowed to substitute ∧ (and) with -> (implies) and ¬ (not)?
For example, if we are asked to show |- p ∧ q, can we show |- ¬(p-> ¬q)
since the 2 formulas are equivalent?

This would only be acceptable if the first formula was considered as
shorthand for the second.

In this context, the question seems to use "∧" as an actual connective
in our formal language, and not just used as shorthand.

Post by Henry S
2. Also, in using Axiom 1-9, can we substitute ◻A for any WFF?
For example, Ax1 is: A->(B->A), so can we write ◻A->(◻B->◻A) as an
application of Ax1?

Yes.

Curtis

[Jonathan Buss]

Post by Curtis Bright

Post by Henry S
1. For assignment 3 question 3 that asks you to do a formal proof, are
we allowed to substitute ∧ (and) with -> (implies) and ¬ (not)?
For example, if we are asked to show |- p ∧ q, can we show |- ¬(p-> ¬q)
since the 2 formulas are equivalent?

This would only be acceptable if the first formula was considered as
shorthand for the second.
In this context, the question seems to use "∧" as an actual connective
in our formal language, and not just used as shorthand.

As Curtis notes, we expected that you would use "∧" directly. But you
may use the ¬(p-> ¬q) form instead, if you prefer. (Either way, you
need a proof.)

Post by Curtis Bright

Post by Henry S
2. Also, in using Axiom 1-9, can we substitute ◻A for any WFF?
For example, Ax1 is: A->(B->A), so can we write ◻A->(◻B->◻A) as an
application of Ax1?

Yes.

Yes, indeed. In modal logic, the set of WFFs includes the ones with boxes.

Similarly, when using first-order logic, the WFFs include the ones with
variables and quantifiers.

Jonathan Buss

[Henry S]

Post by Curtis Bright

Post by Henry S
1. For assignment 3 question 3 that asks you to do a formal proof, are
we allowed to substitute ∧ (and) with -> (implies) and ¬ (not)?
For example, if we are asked to show |- p ∧ q, can we show |- ¬(p-> ¬q)
since the 2 formulas are equivalent?

This would only be acceptable if the first formula was considered as
shorthand for the second.
In this context, the question seems to use "∧" as an actual connective
in our formal language, and not just used as shorthand.

As Curtis notes, we expected that you would use "∧" directly. But you
may use the ¬(p-> ¬q) form instead, if you prefer. (Either way, you need
a proof.)

Post by Curtis Bright

Post by Henry S
2. Also, in using Axiom 1-9, can we substitute ◻A for any WFF?
For example, Ax1 is: A->(B->A), so can we write ◻A->(◻B->◻A) as an
application of Ax1?

Yes.

Yes, indeed. In modal logic, the set of WFFs includes the ones with boxes.
Similarly, when using first-order logic, the WFFs include the ones with
variables and quantifiers.
Jonathan Buss

Thanks for the clarification.

Henry