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
Hi Bill,
Have you tried looking at the HOL Zero source code? I think you will find
it illustrative for your purposes. It has a simple core like HOL Light, but
the source code explains more of what is going on. In file 'corethy.ml' I
try to motivate the axioms and constant definitions used in
Hi Bill,
on 21/3/14 6:19 AM, Bill Richter rich...@math.northwestern.edu wrote:
...
T = ((λxbool . x) = (λxbool . x))
So it looks to me that HOL Light is defining Tom's primitive = in terms of
the Ocaml =. Is that correct? And maybe that just means that the HOL
Light
primitive = is
Bill:
On p 29 of LOGIC, you write that there are constants
Tbool, ∀(α→bool)→bool etc. Why aren't there colons? I would have
written that as
T:bool and ∀:(α→bool)→bool
Are the apparent subscripts supposed to indicate colons, or does HOL4 not
use colons for type annotations?
Throughout the
Thanks, Konrad! I'll read your proof of NOT_FORALL_THM, and try to find Gordon
and Melham's book. Two points:
I don't believe that Church ever explained how typed LC implies FOL. Church
certainly does not explain this in his paper
A Formulation of the Simple Theory of Types
Thanks for correcting me, Mark! I'll look at your HOL Zero source code,
especially corethy.ml. I see my error now. From bool.ml:
let T_DEF = new_basic_definition
`T = ((\p:bool. p) = (\p:bool. p))`;;
The first = is an Ocaml =, but the 2nd =, the one we care about, is the
primitive HOL
The constant = is not defined in HOL Light, but simply declared (as Mark
said). In fact, equality is even more basic than that: it's a built in
term. You can see, for example, the safe_mk_eq function in fusion.ml, and
also the the_term_constants reference (which starts with = built in).
I feel
I should have said '@' instead of '?' here. The constant '?' is actually
defined in these axiomatisations (using '@').
Mark.
on 21/3/14 9:10 AM, Mark Adams m...@proof-technologies.com wrote:
... In HOL Light's axiomatisation, the only such entities are the 'bool'
and
'fun' type constants and
Hi Bill,
on 21/3/14 4:28 PM, Bill Richter rich...@math.northwestern.edu wrote:
... BTW where is the constant = defined in HOL Light? I see now that
the line in bool.ml override_interface (=,`(=):bool-bool-bool`);;
just means that = is being defined as a synonym for = in this special
case.
On 20 Mar 2014, at 16:50, Rob Arthan r...@lemma-one.com wrote:
ProofPower is no different from HOL4 and HOL Light as regards substitution.
The ProofPower documentation does include a formal specification of the logic
and the proof system, but you would probably do better looking at the
[Apologies for multiple copies]
SECOND CALL FOR PAPERS FOR
NATURAL LANGUAGE SERVICES FOR REASONERS (NLSR)
http://vsl2014.at/meetings/NLSR-index.html
July 18, 2014
Affiliated with affiliated to RTA-TLCA
On 20 Mar 2014, at 16:50, Rob Arthan r...@lemma-one.com wrote:
ProofPower is no different from HOL4 and HOL Light as regards substitution.
The ProofPower documentation does include a formal specification of the logic
and the proof system, but you would probably do better looking at the
On Fri, 21 Mar 2014 09:13:41 +
Andrew Butterfield andrew.butterfi...@scss.tcd.ie wrote:
Is this the document kanananaskis-9-logic.pdf?
If it is, I have a query: in Sec 1.1 Introduction (p9) we are shown
some properties
One is *Inhab* : U does not contain empty sets - fair enough
Andrew,
On 21 Mar 2014, at 09:13, Andrew Butterfield andrew.butterfi...@scss.tcd.ie
wrote:
On 20 Mar 2014, at 16:50, Rob Arthan r...@lemma-one.com wrote:
ProofPower is no different from HOL4 and HOL Light as regards substitution.
The ProofPower documentation does include a formal
On Fri, Mar 21, 2014 at 9:08 AM, Bill Richter rich...@math.northwestern.edu
wrote:
Thanks, Konrad! I'll read your proof of NOT_FORALL_THM, and try to find
Gordon and Melham's book. Two points:
I don't believe that Church ever explained how typed LC implies FOL.
Church certainly does not
15 matches
Mail list logo
