Logicism

[dan pittman]

Hi Joe,

I wonder if you'd consider a dependent type theory as a way to make that
distinction more apparent. The notion of "propositions as types" is
pervasive in type theory, however, it is not clear to me how one could
see /all/ types as propositions. E.g. I'm not sure how the Peano
naturals—which is how the definition of the naturals is typically given
in a DTT—could be seen as a proposition, which why I think this relation
goes one way (i.e. not types as propositions). It may also be worth
noting that often times in a type theory, propositions have their own
sort and inhabitants of types of sort Prop are all equal to one another.
More precisely:

if A : Prop, then \forall a, b : A. a \equiv b.

This idea I think is relevant to your question w/r/t to a rigorous way
to make the distinction. With propositions as types, a proposition is
thought to hold intuitionistically: if the type has any inhabitants, its
corresponding proposition is thought to hold. However, the Prop sort
makes this explicit: with Prop, we care only that it /is/ inhabited, not
about the inhabitants themselves.

On 8/11/20 9:00 AM, fom-request at cs.nyu.edu wrote:
> Send FOM mailing list submissions to
> 	fom at cs.nyu.edu
>
> To subscribe or unsubscribe via the World Wide Web, visit
> 	https://cs.nyu.edu/mailman/listinfo/fom
> or, via email, send a message with subject or body 'help' to
> 	fom-request at cs.nyu.edu
>
> You can reach the person managing the list at
> 	fom-owner at cs.nyu.edu
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of FOM digest..."
>
>
> Today's Topics:
>
>    1. Logicism (Joe Shipman)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Mon, 10 Aug 2020 00:19:16 -0400
> From: Joe Shipman <joeshipman at aol.com>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: Logicism
> Message-ID: <BC6D34A3-049F-4ABD-9C92-4E8EFF981327 at aol.com>
> Content-Type: text/plain; charset=utf-8
>
> There seems to be agreement that some mathematical propositions can be shown to be equivalent to truths of logic, and others can?t, but drawing a line between what is ?logical? and what is ?mathematical? is hard.
>
> I?ve had trouble finding a simple, streamlined development of BASIC logicism. Can anyone provide a source for a presentation of a logical system (by which I mean, at the very least, a computable deductive calculus that generates truths of logic) , and an interpretation of theorems of Peano Arithmetic as logical truths in this system?
>
> ? JS
>
> Sent from my iPhone
>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
>
> ------------------------------
>
> End of FOM Digest, Vol 212, Issue 6
> ***********************************