Embed Notice

HTML Code

<blockquote style="position: relative; padding-left: 55px;"><section><a href="https://social.lizzy.rs/users/fleckenstein/statuses/112514489443399783">*(*(void **(*)()) lizzy)()  :v_trans: :v_bi: (fleckenstein@social.lizzy.rs)'s status on Tuesday, 28-May-2024 07:37:08 JST</a><a href="https://social.lizzy.rs/@fleckenstein" title="fleckenstein@social.lizzy.rs"><img src="https://gnusocial.jp/avatar/152098-48-20231121150132.webp" width="48" height="48" alt="*(*(void **(*)()) lizzy)()  :v_trans: :v_bi:" style="position: absolute; left: 0; top: 0;">*(*(void **(*)()) lizzy)()  :v_trans: :v_bi:</a></section><article><p>formal proof of p → (q → r) ⊢ (p → q) → (p → r) in sequence calculus for propositional logic vs formal proof in coq</p></article><footer><a rel="bookmark" href="https://gnusocial.jp/conversation/3153211#notice-6239674">In conversation</a><time datetime="2024-05-28T07:37:08+09:00" title="Tuesday, 28-May-2024 07:37:08 JST">Tuesday, 28-May-2024 07:37:08 JST</time> <span>from <span><a href="https://social.lizzy.rs/@fleckenstein/112514489443399783" rel="external" title="Sent from social.lizzy.rs via ActivityPub">social.lizzy.rs</a></span></span><a href="https://social.lizzy.rs/@fleckenstein/112514489443399783">permalink</a><h4>Attachments</h4><ol><li><label><a rel="external" href="https://gnusocial.jp/attachment/2700901">p → (q → r) ⊢ (p → q) → (p → r)
≡ ¬p ∨ (¬q ∨ r) ⊢ ¬(¬p ∨ q) ∨ (¬p ∨ r) (1) from (Ax) follows: q ⊢ ¬p ∨ r, q
 (2) from (2) and (¬L) follows: q, ¬q ⊢ ¬p ∨ r
 (3) from (Ax) follows: q, r ⊢ ¬p, r
 (4) from (3) and (∨R) follows: q, r ⊢ ¬p ∨ r
 (5) from (2) and (4) and (∨L) follows: q, ¬q ∨ r ⊢ ¬p ∨ r
 (6) from (Ax) follows: q, ¬p ⊢ ¬p, r
 (7) from (6) and (∨R) follows: q, ¬p ⊢ ¬p ∨ r
 (8) from (5) and (7) and (∨L) follows: ¬p ∨ (¬q ∨ r), q ⊢ ¬p ∨ r 
 (9) from (Ax) follows: ¬p ∨ (¬q ∨ r), ¬p ⊢ ¬p, r
(10) from (9) and (∨R) follows: ¬p ∨ (¬q ∨ r), ¬p ⊢ ¬p ∨ r
(11) from (8) and (10) and (∨L) follows: ¬p ∨ (¬q ∨ r), ¬p ∨ q ⊢ ¬p ∨ r
(12) from (11) and (¬R) follows: ¬p ∨ (¬q ∨ r) ⊢ ¬(¬p ∨ q), ¬p ∨ r
(13) from (12) and (∨R) follows: ¬p ∨ (¬q ∨ r) ⊢ ¬(¬p ∨ q) ∨ (¬p ∨ r)QED.</a></label><br><a href="https://social.lizzy.rs/system/media_attachments/files/112/514/460/209/604/856/original/ff109734fb816a17.png" rel="external">https://social.lizzy.rs/system/media_attachments/files/112/514/460/209/604/856/original/ff109734fb816a17.png</a></li><li><label><a rel="external" href="https://gnusocial.jp/attachment/2700902">Definition meow2 p q r : (p -&gt; (q -&gt; r)) -&gt; ((p -&gt; q) -&gt; (p -&gt; r))
  := fun pqr pq p =&gt; pqr p (pq p).</a></label><br><a href="https://social.lizzy.rs/system/media_attachments/files/112/514/487/873/750/755/original/611ce913e1398fc8.png" rel="external">https://social.lizzy.rs/system/media_attachments/files/112/514/487/873/750/755/original/611ce913e1398fc8.png</a></li></ol></footer></blockquote>

Corresponding Notice

Embed this notice
*(*(void **(*)()) lizzy)() :v_trans: :v_bi: (fleckenstein@social.lizzy.rs)'s status on Tuesday, 28-May-2024 07:37:08 JST *(*(void **(*)()) lizzy)() :v_trans: :v_bi:
formal proof of p → (q → r) ⊢ (p → q) → (p → r) in sequence calculus for propositional logic vs formal proof in coq
In conversationTuesday, 28-May-2024 07:37:08 JST from social.lizzy.rspermalink
Attachments
1. p → (q → r) ⊢ (p → q) → (p → r) ≡ ¬p ∨ (¬q ∨ r) ⊢ ¬(¬p ∨ q) ∨ (¬p ∨ r) (1) from (Ax) follows: q ⊢ ¬p ∨ r, q (2) from (2) and (¬L) follows: q, ¬q ⊢ ¬p ∨ r (3) from (Ax) follows: q, r ⊢ ¬p, r (4) from (3) and (∨R) follows: q, r ⊢ ¬p ∨ r (5) from (2) and (4) and (∨L) follows: q, ¬q ∨ r ⊢ ¬p ∨ r (6) from (Ax) follows: q, ¬p ⊢ ¬p, r (7) from (6) and (∨R) follows: q, ¬p ⊢ ¬p ∨ r (8) from (5) and (7) and (∨L) follows: ¬p ∨ (¬q ∨ r), q ⊢ ¬p ∨ r (9) from (Ax) follows: ¬p ∨ (¬q ∨ r), ¬p ⊢ ¬p, r (10) from (9) and (∨R) follows: ¬p ∨ (¬q ∨ r), ¬p ⊢ ¬p ∨ r (11) from (8) and (10) and (∨L) follows: ¬p ∨ (¬q ∨ r), ¬p ∨ q ⊢ ¬p ∨ r (12) from (11) and (¬R) follows: ¬p ∨ (¬q ∨ r) ⊢ ¬(¬p ∨ q), ¬p ∨ r (13) from (12) and (∨R) follows: ¬p ∨ (¬q ∨ r) ⊢ ¬(¬p ∨ q) ∨ (¬p ∨ r) QED.
  https://social.lizzy.rs/system/media_attachments/files/112/514/460/209/604/856/original/ff109734fb816a17.png
2. Definition meow2 p q r : (p -> (q -> r)) -> ((p -> q) -> (p -> r)) := fun pqr pq p => pqr p (pq p).
  https://social.lizzy.rs/system/media_attachments/files/112/514/487/873/750/755/original/611ce913e1398fc8.png

Public

Embed Notice

HTML Code

Corresponding Notice