Thanks, Konrad! You seem to agree with me here, that the typed-LC-implies-FOL
isn't actually important:
My personal feelings on this foundational aspect are that the
actual set of axioms isn't that important provided the usual
introduction and elimination rules of predicate calculus can
My personal feelings on this foundational aspect are that the
actual set of axioms isn't that important provided the usual
introduction and elimination rules of predicate calculus can be
derived from them.
My recollection (don't have citations to hand) is that Church originally
wanted the untyped
Thanks, Rob! I don't Andrew's book to hand either, but his on-line article is
causing me real trouble:
http://plato.stanford.edu/entries/type-theory-church/
1.3.2 Elementary Type Theory
We start by listing the axioms for what we shall call elementary type theory.
(1) [pο ∨ pο] ⊃ pο
Bill,
On 19 Mar 2014, at 07:02, Bill Richter wrote:
> work is. If I understood it, I'm sure I'd say it was elegant mathematics,
> and that it's good we're assuming the weakest possible set of axioms.
Have you looked at Peter Andrews’ book "An Introduction to Mathematical Logic
and Type The
FMCAD 2014 - FORMAL METHODS IN COMPUTER-AIDED DESIGN
FIRST CALL FOR PAPERS
International Conference on
Formal Methods in Computer-Aided Design (FMCAD)
Lausanne, Switzerland, October 21-24, 2014
http://www.fmcad.org/FMCAD14
The conference includes the FMCAD student forum;
it is collocated with
Please find the NFM 2014 Call for Participation below. With no
registration fee and very reasonable costs for accommodations this
conference is an excellent value to attend even without presenting a
paper. It is also a great place to bring students for exposure to
real-world applications!
***
ICTAC 2014 will be held in Bucharest during 17-20 September,
followed by SYNASC 2014 in Timisoara 22-25 September 2014.
[Apologies if you receive multiple copies of this message]
-
Abstract submission: 30 March 2014 (extende
** We apologize for multiple copies of this CFP **
* *
* Call for papers *
*
