From: Dusko Pavlovic <dusko@kestrel.edu>
To: Steve Vickers <s.j.vickers@cs.bham.ac.uk>,
Categories list <categories@mta.ca>
Cc: Vaughan Pratt <pratt@cs.stanford.edu>
Subject: Re: Empty algebras
Date: Sun, 23 Oct 2011 22:11:38 +0100 [thread overview]
Message-ID: <E1RIJcX-00026V-4t@mlist.mta.ca> (raw)
In-Reply-To: <E1RHwoL-0003lH-Ba@mlist.mta.ca>
> variable a. To avoid the vacuity and get a falsehood you have to
> quantify out the free variable, as
>
> ((all) a. P(a)) --> ((exists) x. P(x))
here is a proof of this apparent falsehood:
(all) a. P(a) --> (all) b. P(b) (exists) b. P(b) --> (exists) x. P(x)
-------------------------------- -------------------------------------
(all) a. P(a) --> P(b) P(b) --> (exists) x. P(x)
---------------------------------------------------------------------------------------
(all) a. P(a) --> (exists) x. P(x)
(it's is just adjunctions in foundations again: we compose the counit of the adjunction of one quantifier with the unit of the other one. note that it is valid constructively. i am not sure, but i think gentzen gave a different proof in an example.)
-- dusko
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
next prev parent reply other threads:[~2011-10-23 21:11 UTC|newest]
Thread overview: 20+ messages / expand[flat|nested] mbox.gz Atom feed top
2011-10-20 12:40 Michael Barr
2011-10-21 14:23 ` Steve Vickers
[not found] ` <4EA1807A.1060802@cs.bham.ac.uk>
2011-10-21 22:06 ` Vaughan Pratt
2011-10-22 13:03 ` Steve Vickers
2011-10-23 18:04 ` Vaughan Pratt
2011-10-23 21:11 ` Dusko Pavlovic [this message]
[not found] ` <CE271049-EF59-4E64-AAEA-C1A673FEA224@kestrel.edu>
2011-10-24 7:20 ` Vaughan Pratt
2011-10-24 9:53 ` Steve Vickers
[not found] ` <5E279F28-70B7-4393-A564-B95E3768C561@cs.bham.ac.uk>
2011-10-24 12:35 ` Dusko Pavlovic
[not found] ` <36141083-FB05-4179-8C98-81D5D6EBB6B1@kestrel.edu>
2011-10-24 13:57 ` Steve Vickers
2011-10-25 14:38 ` Michael Barr
[not found] ` <Pine.LNX.4.64.1110251036240.25129@msr03.math.mcgill.ca>
2011-10-25 16:09 ` Steve Vickers
2011-10-25 18:02 ` Vaughan Pratt
2011-10-26 10:11 ` Steve Vickers
2011-10-27 10:08 ` Vaughan Pratt
2011-10-30 16:44 ` Steve Vickers
2011-10-26 10:46 ` Andrej Bauer
2011-10-26 11:31 ` Paul Levy
[not found] ` <BDB34A2E-CCD4-4F41-AE9E-B865F2DF4872@cs.bham.ac.uk>
2011-10-24 16:47 ` Dusko Pavlovic
2011-10-22 22:36 ` Dusko Pavlovic
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=E1RIJcX-00026V-4t@mlist.mta.ca \
--to=dusko@kestrel.edu \
--cc=categories@mta.ca \
--cc=pratt@cs.stanford.edu \
--cc=s.j.vickers@cs.bham.ac.uk \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).