Path: csiph.com!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mostowski Collapse <janburse@fastmail.fm>
Newsgroups: comp.lang.prolog
Subject: Re: France is the Fire Nation of Prolog
Date: Fri, 31 Dec 2021 01:11:36 +0100
Message-ID: <sqlhro$bqho$1@solani.org>
References: <d1ab4350-9a9d-49bc-845b-f10eeb1ec763n@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 31 Dec 2021 00:11:36 -0000 (UTC)
Injection-Info: solani.org; logging-data="387640"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:68.0) Gecko/20100101 Firefox/68.0 SeaMonkey/2.53.10.2
Cancel-Lock: sha1:fSDY5WMTyC+PewQaNey3TMjB0JI=
X-User-ID: eJwNycEBwEAEBMCWzmJJOY7ov4RkvuNKYYfRab6+URicdoyiE+irOxJXsPGfPTbX+GIySD2xh12+lUh3Sn1IXxT4
In-Reply-To: <d1ab4350-9a9d-49bc-845b-f10eeb1ec763n@googlegroups.com>
Xref: csiph.com comp.lang.prolog:12515

Lean TAP can be fun. Spent the whole day to
render MathJax. Then was annoyed by MathJax,
how do you put this thingy into an email?

So here is barber paradox in list form with Unicode:

1. s(a,a) ⊢ s(a,a) (ax)
2. s(a,a) ⊢ ∃zs(z,z) (R∃)
3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
4. s(a,a) ⊢ s(a,a) (ax)
5. s(a,a) ⊢ ∃zs(z,z) (R∃)
6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)

http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html