使用SML与HOL推理规则证明定理[] |- p /\ q <=> q /\ p的问题

Nice try on proving conjunction commutativity! The issue with your current code is that you’re adding p and q as explicit assumptions, which stick around in the final theorem. Instead, you should derive p and q from the conjunction assumptions using HOL’s elimination rules. Here’s how to adjust your approach:

Step-by-Step Breakdown #

1. Prove the forward implication: Start by assuming p ∧ q, then extract p and q using CONJUNCT1 and CONJUNCT2. Use these to prove q ∧ p, then discharge the initial assumption to get (p ∧ q) ⇒ (q ∧ p) (no premises left here!).
2. Prove the reverse implication: Do the same in reverse—assume q ∧ p, extract q and p, prove p ∧ q, discharge to get (q ∧ p) ⇒ (p ∧ q).
3. Combine the two implications: Use IMP_ANTISYM_RULE to turn the two one-way implications into a biconditional with no premises.

Corrected SML Code #

-- Forward direction: (p ∧ q) → (q ∧ p)
val assume_pq = ASSUME ``p:bool ∧ q:bool``;
val thm_p = CONJUNCT1 assume_pq;  -- Get p from p ∧ q
val thm_q = CONJUNCT2 assume_pq;  -- Get q from p ∧ q
val thm_qp = CONJ thm_q thm_p;    -- Prove q ∧ p
val forward_impl = DISCH ``p:bool ∧ q:bool`` thm_qp;

-- Reverse direction: (q ∧ p) → (p ∧ q)
val assume_qp = ASSUME ``q:bool ∧ p:bool``;
val thm_q_rev = CONJUNCT1 assume_qp;  -- Get q from q ∧ p
val thm_p_rev = CONJUNCT2 assume_qp;  -- Get p from q ∧ p
val thm_pq = CONJ thm_p_rev thm_q_rev;-- Prove p ∧ q
val reverse_impl = DISCH ``q:bool ∧ p:bool`` thm_pq;

-- Final biconditional
val conj_comm_thm = IMP_ANTISYM_RULE forward_impl reverse_impl;

What Changed? #

Instead of assuming p and q directly, we extract them from the conjunction assumption using CONJUNCT1 and CONJUNCT2. This means we don’t add any extra premises to our proof. When we discharge the initial conjunction assumption with DISCH, the resulting implications have no leftover premises. Combining these two implications gives you the desired premise-free theorem: [] |- p ∧ q <=> q ∧ p.

内容的提问来源于stack exchange，提问作者Tuffie