Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: logical inference
Replies: 1   Last Post: Nov 16, 2012 7:48 PM

 Graham Cooper Posts: 4,495 Registered: 5/20/10
Re: logical inference
Posted: Nov 16, 2012 7:48 PM

On Nov 17, 2:43 am, Frederick Williams <freddywilli...@btinternet.com>
wrote:
> RichD wrote:
>

> > I saw on another board, someone said that the rules of inference for
> > second order logic are unknown, actually undecidable.  Which means
> > we have no way to check proofs?

>
> > Can anyone explain or expand on this?
>
> You may wish to read
> https://en.wikipedia.org/wiki/Second_order_logic#Metalogical_results.
>

That's exactly what I said!

Metalogical results

It is a corollary of Gödel's incompleteness theorem that there is
no
deductive system (that is, no notion of provability) for second-
order
formulas that simultaneously satisfies these three desired
attributes

(Soundness) Every provable second-order sentence is universally
valid, i.e., true in all domains under standard semantics.

(Completeness) Every universally valid second-order formula, under
standard semantics, is provable.

(Effectiveness) There is a proof-checking algorithm that can
correctly
decide whether a given sequence of symbols is a valid proof or not.

[HERC]
In that case proofs about 2OL formula would tend to be consistency
and closure proofs, so I imagine Godel's Statement is the reason for
what you heard.

I just prefaced it with a warning that ZUHAIR et al. call 2OL
ranging over uncountable sets

============================================

FINE I'll take all my new Logic Technology elsewhere if that's the
treatment I get for advancing the field..

1/ ENCODING A(X) as a subset predicate { x | D(x) } C { x |
P(x) }

2/ ITERATIVE BACKTRACKING SOLVER that will work with 1 SQL JOIN QUERY
to do all the predicate matching.

vert ( pnt( 1,2 ) pnt( 1,4 ) )

This will be
ID REF FIELD TYP
=================
1 11 vert H
1 12 pnt P
1 13 pnt P
1 121 1 T
1 122 2 T
1 131 1 T
1 132 4 T

vert ( pnt( X,Y ) pnt( X,Z ) )
ID REF FIELD TYP
=================
21 11 vert H
21 12 pnt P
21 13 pnt P
21 121 X V
21 122 Y V
21 131 X V
21 132 Z V

Something like

SELECT * FROM TTAILS, TPRO
WHERE TTAILS.REF = TPRO.REF
AND TTAILS.FIELD = TPRO.FIELD
GROUP BY ID
ORDER BY ID DESCENDING

This performs 5 pages of coding for UNIFY(f1, f2) in 5 lines of SQL!

Butt... since ACTUAL WORKING FORMAL SYSTEMS written in predicates