On 11/27/2024 04:06 AM, Julio Di Egidio wrote:
On 27/11/2024 04:02, Ross Finlayson wrote:
On 11/22/2024 09:30 AM, Julio Di Egidio wrote:
On 22/11/2024 18:23, Julio Di Egidio wrote:
On 19/11/2024 14:55, Mild Shock wrote:
```
?- solve_trace([p->q,r->s,p\/r]=>q\/s, Qs).
```
>
Never mind, I have fixed it: just needed to get rid of those `once`!
Will update the Gist shortly.
>
If you have any feedback already, it's very welcome: anyway, will keep
you guys posted.
>
Good afternoon, what is this about briefly?
>
Hi Ross, it's a little linear propositional solver at this stage, but
with ambitions...
>
See here:
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
>
Julio
>
Hallo Julio, well then warm regards.
The "intuitionistic", reflects mostly part of the dialectic,
thesis/antithesis/synthesis, the anti-thesis part, grounded
on its own ideals, then when later combined, what's new is
old again - intuitionism today is either theory tomorrow
or gathering dust in the basement of Hilbert's Infinite Living
Working Museum the speculative theories.
The, "axiomless", then, natural deduction, is what I think you mean
when you say "intuitionistic", natural deduction, then that deduction
is a very thorough sort of idea - with both "abstraction" and
generalization and "reduction" and simplification or mathematics
the theory the practice.
Here it's considered to demand a brief metaphysics and the
establishment of a putative true, complete, consistent theory,
a "mere metaphysics", that's though the theory, with nothing/everything
then universals and point/space and "axiomless natural geometry".
It seems definitely so that "material implication" of course is
excluded from a true monotone, modal theory with
free/unrestricted/many-ordered monotonicity and modality and entailment.
The "material
implication" or "quasi-modal" is furthermore considered "post-classical"
or "quasi-classical".
Then, for solvers like those of the day, or Mizar or Metamath or
Coq given types or Lean or what, then there's probably still one
thing about "infinite-union" versus "pair-wise union", the illative
or univalent, with regards to a theory being a sort of, "heno-theory",
that is one theory and one model, then variously in perspective,
for example a set theory and/or a part theory, each of those
set up in universals.
This of course involves quantifier disambiguation for universals
and predicativity for universals and these kinds of things,
and the "extra-ordinary" as natural, vis-a-vis super _natural_,
and _super_ natural, natural.
You can find my podcasts I've setup an approach to nouveau mechanics,
and been getting into "Foundations" rather usually.
https://www.youtube.com/@rossfinlaysonSo, modal and "thorough", relevance logic, given a deductive goal
to attain to to arrive at, makes for a "fuller dialectic" then
why inductive inference has that its partial and can't fulfill
itself, or after for example Goodman's "A Riddle of Induction",
then why "axiomless natural deduction" sorts out for a strong
mathematical platonism and strong (not weak) logicist positivism,
together, and first for a sort of, "axiomless geometry", via,
"axiomless natural deduction", since stipulations are unfounded.
Of course a variety of what are "non-standard", results, according
to the standard, are standard again, establishing the very ideals
and "goals" of inference, intuitionistic in the sense of a
"fuller dialectic".
Warm regards, Ross
How to prove this theorem with intuitionistic natural deduction?
Re: can λ-prolog do it? (Was: How to prove this theorem with intuitionistic natural deduction?)