Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Free variables aren't quantified, it's that si...

Email Gateway (Aug 19 2022 at 08:36):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
It sort of escaped my notice that although I have

theorem --"(4)"
"(!C.!D.(C | D --> C)) --> (A | B --> A)"
by auto

I also have anything else I want to prove, for the simple fact that the
hypothesis is always false.

theorem --"(4a)"
"(!C.!D.(C | D --> C)) --> P a"
by auto

This could be material for my book, "How to Learn Basic Logic with
Isabelle", or with the type of title I always hate, "Logic for Dummies
with Isabelle2012".
http://www.amazon.com/Logic-For-Dummies-Mark-Zegarelli/dp/0471799416

It still appears that free variables aren't quantified, although my
reasoning might be warped. It may not be warped. If I just know what's
true, then I can sometimes straighten out my reasoning.

This is my first use of Isabelle as a tool to confirm some basic logic.
No one else is going to take any substantial time to clarify and remind
me of the basics that I mostly understand. There's nothing wrong with that.

Regards,
GB

Email Gateway (Aug 19 2022 at 08:36):

From: Alfio Martini <alfio.martini@acm.org>

Hi Gottfried,

I was more than convinced by the following answer from Paulson, stated in a
previous e-mail (assuming
my simpler question subsumes the one you posed):

The formula (?x + ?y) + ?z = ?x + (?y + ?z) expresses a property about

three quantities denoted by ?x, ?y and ?z. It is a convention in logic that
any theorem involving free variables denotes the "universal closure" of
that formula, here
"all x. all y. all y. (x+y)+z = x + (y+z)".
Isabelle is designed to work best a minimum of logical symbols, hence the
preference for stating theorems like
P1 ==> … Pn ==> Q.
Hardly any mathematics paper states such theorems as
!x1 … xm. P1 & … & Pn —> Q.

So, they do not get quantified, but they have the same "denotation" (that
is to say, they are equivalent
under all interpretations.)

All the Best!
On Fri, Sep 14, 2012 at 1:52 AM, Gottfried Barrow
<gottfried.barrow@gmx.com>wrote:

Hello,

I break this out so the simple point doesn't get lost in the noise I
created from the last thread.

The question was: What's the difference between free variables and
universally quantified variables?

A partial answer is: Free variables don't get quantified.

The software gave me the answer to my question. Propositions, tautologies,
contradictions. When a formula with free variables is a tautology or a
contradiction, then it's equivalent to a quantified form of the same
formula. If it's not a tautology or contradiction, then there's no
equivalency. It's that simple, at least for my simple cases.

The use of the phrase "free variable" is all over the place:
http://en.wikipedia.org/wiki/**Free_variables_and_bound_**variables<http://en.wikipedia.org/wiki/Free_variables_and_bound_variables>

In the context of FOL, you have formulas with free variables, but then you
put them in other formulas in which the variables get bound:
http://en.wikipedia.org/wiki/**First-order_logic<http://en.wikipedia.org/wiki/First-order_logic>

"A formula in first-order logic with no free variables is called
a*first-ordersentence <http://en.wikipedia.org/wiki/**
Sentence_%28mathematical_**logic%29<http://en.wikipedia.org/wiki/Sentence_%28mathematical_logic%29>>*.
These are the formulas that will have well-definedtruth values <
http://en.wikipedia.org/wiki/**Truth_value<http://en.wikipedia.org/wiki/Truth_value>>under
an interpretation."

This wasn't a case where I needed to study any logic. The stuff I need to
study is not this basic, discrete math level logic. I was making the wrong
assumptions, and I also needed to sync up some vocabulary, and maybe have
my mind refreshed just a little on stuff I haven't used on a daily basis.

If I'm still wrong, all I can do, when the documentation doesn't cover a
topic, is make conclusions based on what I get the software to do. The
theorems below gave me the data to say what I said above.

If "free variables don't get quantified" is supposed to be obvious because
of "free variables", it isn't. I gave the quote above, plus I had asked the
question, and I never got a simple, authoritative answer saying, "Free
variables don't get quantified".

Regards,
GB

theorem --"(1)"
--"As a test case, I show a quantified and free form equivalency, for a
true
proposition that's a tautology."
"(A & B --> A) <-> (!C.!D.(C & D --> C))"
by auto

theorem --"(2)"
--"I then negate the formula inside the quantified variables, to show that
a
false proposition works as well, when it's a contradiction."
"~(A & B --> A) <-> (!C.!D.~(C & D --> C))"
by auto

theorem --"(3)"
--"I then try to show an equivalency with another proposition that is
neither a tautology or contradiction. A counterexample is found."
"(A | B --> A) <-> (!C.!D.(C | D --> C))"
--"Nitpick found a counterexample:
Free variables:
(A?bool) = True
(B?bool) = False"
oops

theorem --"(4)"
--"It turns out, free variable formulas are propositions. So a free
variable
formula is a tautology if a quantified form of it is proved to be true.
Here
the software doesn't care that the LHS and the RHS is false."
"(!C.!D.(C | D --> C)) --> (A | B --> A)"
by auto

theorem --"(5)"
--"Here, the LHS is not quantified in any way, shape, or form, so it can't
be
used to prove the RHS."
"(A | B --> A) --> (!C.!D.(C | D --> C))"
--"Nitpick found a counterexample:
Free variables:
(A?bool) = True
(B?bool) = False
Skolem constants:
(C?bool) = False
(D?bool) = True"
oops

Email Gateway (Aug 19 2022 at 08:36):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 9/14/2012 6:13 PM, Alfio Martini wrote:

I was more than convinced by the following answer from Paulson, stated in a
previous e-mail (assuming my simpler question subsumes the one you posed):

The formula (?x + ?y) + ?z = ?x + (?y + ?z) expresses a property about
three quantities denoted by ?x, ?y and ?z. It is a convention in logic that

any theorem involving free variables denotes the "universal closure" of
that formula,

Alfio,

You say, "assuming my simpler question subsumes the one you posed".

I'm pretty sure it doesn't. Please notice that I never use the schematic
variable notation, whereas you and Larry do.

(On that email, it was to you, but I replied to Larry as if it was to
me, which I thought it was, but I apologize for that.)

I've been asking about the relationship between free variables and
quantified variables in a formula prior to the formula being proved
(although some of my tangents involved proofs). I think you and Larry
are talking about formulas that have been proved.

It might be so obvious to people that free variables don't get
quantified that everyone thought I was talking about post-proof free
variables in a proved theorem.

First-order logic polluted my mind. I had the idea that any free
variable in P gets implicitly bound by the prover engine when I put P in
the statement theorem "P". It makes sense now that it wouldn't.
Propositions are more general than closed formulas.

According to the tutorial, free variables get converted to schematic
variables after a proof (page 7 tutorial.pdf). There is "free variable"
pre-proof, and "free/schematic variable" post-proof.

I was talking about free variables in the mere statement of a theorem, like,

theorem --"(3)"
"(A | B --> A)<-> (!C.!D.(C | D --> C))"
oops

For (3), I now call the left-hand side a proposition, and I think of it
in terms of propositional logic. I call the right-hand side a closed
formula, and I think of it terms of first-order logic. A proposition
does not necessarily have a definite truth value, whereas a closed
formula does. That's what I showed below with my 5 examples.

So, they do not get quantified, but they have the same "denotation" (that
is to say, they are equivalent under all interpretations.)

So you would appreciate Larry's explanation more than me because I don't
know anything about interpretations. My interpretation is that
everything resolves to a boolean value of either true or false, based on
my basic understanding of logical connectives and quantifiers.

Regards,
GB

On Fri, Sep 14, 2012 at 1:52 AM, Gottfried Barrow
<gottfried.barrow@gmx.com>wrote:

Hello,

I break this out so the simple point doesn't get lost in the noise I
created from the last thread.

The question was: What's the difference between free variables and
universally quantified variables?

A partial answer is: Free variables don't get quantified.

The software gave me the answer to my question. Propositions, tautologies,
contradictions. When a formula with free variables is a tautology or a
contradiction, then it's equivalent to a quantified form of the same
formula. If it's not a tautology or contradiction, then there's no
equivalency. It's that simple, at least for my simple cases.

The use of the phrase "free variable" is all over the place:
http://en.wikipedia.org/wiki/**Free_variables_and_bound_**variables<http://en.wikipedia.org/wiki/Free_variables_and_bound_variables>

In the context of FOL, you have formulas with free variables, but then you
put them in other formulas in which the variables get bound:
http://en.wikipedia.org/wiki/**First-order_logic<http://en.wikipedia.org/wiki/First-order_logic>

"A formula in first-order logic with no free variables is called
a*first-ordersentence<http://en.wikipedia.org/wiki/**
Sentence_%28mathematical_**logic%29<http://en.wikipedia.org/wiki/Sentence_%28mathematical_logic%29>>*.
These are the formulas that will have well-definedtruth values<
http://en.wikipedia.org/wiki/**Truth_value<http://en.wikipedia.org/wiki/Truth_value>>under
an interpretation."

This wasn't a case where I needed to study any logic. The stuff I need to
study is not this basic, discrete math level logic. I was making the wrong
assumptions, and I also needed to sync up some vocabulary, and maybe have
my mind refreshed just a little on stuff I haven't used on a daily basis.

If I'm still wrong, all I can do, when the documentation doesn't cover a
topic, is make conclusions based on what I get the software to do. The
theorems below gave me the data to say what I said above.

If "free variables don't get quantified" is supposed to be obvious because
of "free variables", it isn't. I gave the quote above, plus I had asked the
question, and I never got a simple, authoritative answer saying, "Free
variables don't get quantified".

Regards,
GB

theorem --"(1)"
--"As a test case, I show a quantified and free form equivalency, for a
true
proposition that's a tautology."
"(A& B --> A)<-> (!C.!D.(C& D --> C))"
by auto

theorem --"(2)"
--"I then negate the formula inside the quantified variables, to show that
a
false proposition works as well, when it's a contradiction."
"~(A& B --> A)<-> (!C.!D.~(C& D --> C))"
by auto

theorem --"(3)"
--"I then try to show an equivalency with another proposition that is
neither a tautology or contradiction. A counterexample is found."
"(A | B --> A)<-> (!C.!D.(C | D --> C))"
--"Nitpick found a counterexample:
Free variables:
(A?bool) = True
(B?bool) = False"
oops

theorem --"(4)"
--"It turns out, free variable formulas are propositions. So a free
variable
formula is a tautology if a quantified form of it is proved to be true.
Here
the software doesn't care that the LHS and the RHS is false."
"(!C.!D.(C | D --> C)) --> (A | B --> A)"
by auto

theorem --"(5)"
--"Here, the LHS is not quantified in any way, shape, or form, so it can't
be
used to prove the RHS."
"(A | B --> A) --> (!C.!D.(C | D --> C))"
--"Nitpick found a counterexample:
Free variables:
(A?bool) = True
(B?bool) = False
Skolem constants:
(C?bool) = False
(D?bool) = True"
oops

Email Gateway (Aug 19 2022 at 08:36):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
Alfio,

To try and summarize it, for you "they" are the formulas with free
variables that get proved. I'm going to label these propositions that
you're talking about as tautologies. They have the same denotation as
some quantified formula.

For me, "they" are the formulas with free variables which have no
definite truth value, like the (3) that I gave as an example. For these
formulas, there is not an equivalent quantified formula.

You're focusing on the free variable formulas that can be proved, and
their equivalency to a quantified formula.

I'm focusing on the free variable formulas that can't be proved, and
which don't have an equivalency to a quantified formula.

I think that's the way it is.

Regards,
GB

Email Gateway (Aug 19 2022 at 08:37):

From: Alfio Martini <alfio.martini@acm.org>
Hi Gottfried,

You say, "assuming my simpler question subsumes the one you posed".

I'm pretty sure it doesn't. Please notice that I never use the schematic
variable notation, whereas you and Larry do.

You are right, I missed that.

For (3), I now call the left-hand side a proposition, and I think of it in

terms of propositional logic. I call the right-hand side a closed formula,
and I think of it terms of first-order logic. A proposition does not
necessarily have a definite truth value, whereas a closed formula does

I understand that a proposition is the same thing as sentence, as it is
often called and thus has
to have a definite logical truth-value. In this way, I always comeback to
the definition of interpretation. In first-order logic
an interpretation assigns meanings only to the syntactic entities [of the
signature or basis].
Meaning of free variables are fixed by the notion of a state, i.e., a
function from variables to values.

So, in first-order logic, any formula that contains [for instance] a
free-variable
"x" it is not [be called] a proposition, and it is actually a function(al)
on that free-variable. It can be seen as having the
type State=>Bool, where State is a function Vars=>D, Vars is the set of
variables used to build the set
of well-formed formulas and D is the domain in question. In this sense, the
truth-value of this formula
is open. It depends on the value of this free variable. It does not assert
anything.

Now, propositional logic is just a sublogic of first-order logic, with no
function symbols and where all predicate symbols
have arity zero. The "variables" here are just predicates. Thus, it is
enough to fix an interpretation for these predicates in
order to have the definite truth-value of the expression. So, from
this point of view, every well-formed expression in propositional logic is
a assertion, i.e., a sentence. That is why,
I think, it can be called propositional or sentential logic.

I am not sure if this view (as written above) is shared by other people,
though.

All the Best!

On Sat, Sep 15, 2012 at 12:30 AM, Gottfried Barrow <gottfried.barrow@gmx.com

wrote:

On 9/14/2012 6:13 PM, Alfio Martini wrote:

I was more than convinced by the following answer from Paulson, stated in
a
previous e-mail (assuming my simpler question subsumes the one you posed):

The formula (?x + ?y) + ?z = ?x + (?y + ?z) expresses a property about
three quantities denoted by ?x, ?y and ?z. It is a convention in logic
that

any theorem involving free variables denotes the "universal closure"
of
that formula,

Alfio,

You say, "assuming my simpler question subsumes the one you posed".

I'm pretty sure it doesn't. Please notice that I never use the schematic
variable notation, whereas you and Larry do.

(On that email, it was to you, but I replied to Larry as if it was to me,
which I thought it was, but I apologize for that.)

I've been asking about the relationship between free variables and
quantified variables in a formula prior to the formula being proved
(although some of my tangents involved proofs). I think you and Larry are
talking about formulas that have been proved.

It might be so obvious to people that free variables don't get quantified
that everyone thought I was talking about post-proof free variables in a
proved theorem.

First-order logic polluted my mind. I had the idea that any free variable
in P gets implicitly bound by the prover engine when I put P in the
statement theorem "P". It makes sense now that it wouldn't. Propositions
are more general than closed formulas.

According to the tutorial, free variables get converted to schematic
variables after a proof (page 7 tutorial.pdf). There is "free variable"
pre-proof, and "free/schematic variable" post-proof.

I was talking about free variables in the mere statement of a theorem,
like,

theorem --"(3)"

"(A | B --> A)<-> (!C.!D.(C | D --> C))"
oops

For (3), I now call the left-hand side a proposition, and I think of it in
terms of propositional logic. I call the right-hand side a closed formula,
and I think of it terms of first-order logic. A proposition does not
necessarily have a definite truth value, whereas a closed formula does.
That's what I showed below with my 5 examples.

So, they do not get quantified, but they have the same "denotation" (that

is to say, they are equivalent under all interpretations.)

So you would appreciate Larry's explanation more than me because I don't
know anything about interpretations. My interpretation is that everything
resolves to a boolean value of either true or false, based on my basic
understanding of logical connectives and quantifiers.

Regards,
GB

On Fri, Sep 14, 2012 at 1:52 AM, Gottfried Barrow

<gottfried.barrow@gmx.com>**wrote:

Hello,

I break this out so the simple point doesn't get lost in the noise I
created from the last thread.

The question was: What's the difference between free variables and
universally quantified variables?

A partial answer is: Free variables don't get quantified.

The software gave me the answer to my question. Propositions,
tautologies,
contradictions. When a formula with free variables is a tautology or a
contradiction, then it's equivalent to a quantified form of the same
formula. If it's not a tautology or contradiction, then there's no
equivalency. It's that simple, at least for my simple cases.

The use of the phrase "free variable" is all over the place:
http://en.wikipedia.org/wiki/*Free_variables_and_bound_*variables<http://en.wikipedia.org/wiki/**Free_variables_and_bound_**variables>
<http://en.wikipedia.org/wiki/Free_variables_and_bound_variables<http://en.wikipedia.org/wiki/Free_variables_and_bound_variables>
>

In the context of FOL, you have formulas with free variables, but then
you
put them in other formulas in which the variables get bound:
http://en.wikipedia.org/wiki/****First-order_logic<http://en.wikipedia.org/wiki/**First-order_logic>
<http://en.wikipedia.org/wiki/First-order_logic<http://en.wikipedia.org/wiki/First-order_logic>
>

"A formula in first-order logic with no free variables is called
a*first-ordersentence<http://en.wikipedia.org/wiki/<http://en.wikipedia.org/wiki/**>
Sentence_%28mathematical_**logic%29<http://en.wikipedia.
org/wiki/Sentence_%**28mathematical_logic%29<http://en.wikipedia.org/wiki/Sentence_%28mathematical_logic%29>

*.

These are the formulas that will have well-definedtruth values<
http://en.wikipedia.org/wiki/****Truth_value<http://en.wikipedia.org/wiki/**Truth_value>
<http://en.**wikipedia.org/wiki/Truth_value<http://en.wikipedia.org/wiki/Truth_value>
**>>under

an interpretation."

This wasn't a case where I needed to study any logic. The stuff I need to
study is not this basic, discrete math level logic. I was making the
wrong
assumptions, and I also needed to sync up some vocabulary, and maybe have
my mind refreshed just a little on stuff I haven't used on a daily basis.

If I'm still wrong, all I can do, when the documentation doesn't cover a
topic, is make conclusions based on what I get the software to do. The
theorems below gave me the data to say what I said above.

If "free variables don't get quantified" is supposed to be obvious
because
of "free variables", it isn't. I gave the quote above, plus I had asked
the
question, and I never got a simple, authoritative answer saying, "Free
variables don't get quantified".

Regards,
GB

theorem --"(1)"
--"As a test case, I show a quantified and free form equivalency, for a
true
proposition that's a tautology."
"(A& B --> A)<-> (!C.!D.(C& D --> C))"

by auto

theorem --"(2)"
--"I then negate the formula inside the quantified variables, to show
that
a
false proposition works as well, when it's a contradiction."
"~(A& B --> A)<-> (!C.!D.~(C& D --> C))"

by auto

theorem --"(3)"
--"I then try to show an equivalency with another proposition that is
neither a tautology or contradiction. A counterexample is found."
"(A | B --> A)<-> (!C.!D.(C | D --> C))"
--"Nitpick found a counterexample:
Free variables:
(A?bool) = True
(B?bool) = False"
oops

theorem --"(4)"
--"It turns out, free variable formulas are propositions. So a free
variable
formula is a tautology if a quantified form of it is proved to be
true.
Here
the software doesn't care that the LHS and the RHS is false."
"(!C.!D.(C | D --> C)) --> (A | B --> A)"
by auto

theorem --"(5)"
--"Here, the LHS is not quantified in any way, shape, or form, so it
can't
be
used to prove the RHS."
"(A | B --> A) --> (!C.!D.(C | D --> C))"
--"Nitpick found a counterexample:
Free variables:
(A?bool) = True
(B?bool) = False
Skolem constants:
(C?bool) = False
(D?bool) = True"
oops

Email Gateway (Aug 19 2022 at 08:38):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 9/16/2012 10:00 AM, Alfio Martini wrote:

For (3), I now call the left-hand side a proposition, and I think of it in terms of propositional logic. I call the right-hand side a closed formula, and I think of it terms of first-order logic. A proposition does not necessarily have a definite truth value, whereas a closed formula does
I understand that a proposition is the same thing as sentence, as it is often called and thus has to have a definite logical truth-value. In this way, I always comeback to the definition of interpretation.

Dear Alfio,

(Another long email, so I put this here at the top. I work out ideas
with these type of emails, but I also consider "involved technical
discussions by text" as acts in frustration. You can have the last word,
if you want the last word. My reply here is long enough to where I don't
even want to read it to proof it one final time.)

First, my logic vocabulary is messed up in a lot of ways, but I also
think we're running into some legitimate vocabulary problems.

(I'd be happy to sit under you in Brasil to help straighten me out, but
Brasil sounds expensive, and I'm not a programmer, I already see my name
too much, so I don't reply to emails like "Re: [isabelle] Eliminating
two quantifiers in structural proof", and say, "Alfio, very useful
examples. Thanks".)

Isabelle/HOL "subsumes", naively or formally, many different formalized
logics. These logics all have a different, though similar, vocabulary,
and two of these logics are propositional logic and first-order logic.

I was taking "sentence" from first-order logic, which is formally
defined to be a formula with no free variables.

For "definite truth value", I meant that no matter what the assignment
of truth values to a sentence's FOL atomic formulas, a FOL sentence has
only one truth value. For a proposition, the truth value of the
proposition may vary depending on the assignment of truth values to its
atomic formulas. You cover those ideas below.

My standard text for propositional and first-order logic is Bilaniuk's
"A Problem Course in Mathematical Logic", from which I have and will
continue to get my vocabulary, one reason is the book is free and
online, and another is that I like his choice of words; below, I refer
to it as "Bilaniuk":

http://euclid.trentu.ca/math/sb/pcml/pcml.html

For this email, I supplement it with this article:

http://logic.stanford.edu/classes/cs157/2011/notes/chap02.html

Continuing with your comments:

In first-order logic an interpretation assigns meanings only to the syntactic entities [of the
signature or basis]. Meaning of free variables are fixed by the notion of a state, i.e., a function from variables to values.

But Alfio, now you're at a level of formalism that's not workable for
people with a formal education in mathematics at the undergraduate
level, where I would have an undergraduate_plus level of education. I'm
learning something here, and my use of "interpretation" might be
necessary, but formalism that I can't pass on to lots of other people is
of limited use to me.

So, in first-order logic, any formula that contains [for instance] a
free-variable"x" it is not [be called] a proposition, and it is actually a function(al)
on that free-variable. It can be seen as having the type State=>Bool, where State is a function Vars=>D, Vars is the set of variables used to build the set of well-formed formulas and D is the domain in question. In this sense, the truth-value of this formula is open. It depends on the value of this free variable. It does not assert anything.

I understand what you're saying, but in the context of Isabelle/HOL,
below I argue about "it is not to be called a proposition". (Below, I
see I didn't exactly address that "I can consider open FOL formulas as
propositions".)

I guess we're still talking about this formula, and you're saying it's open:

theorem --"(3)"
"(A | B --> A)<-> (!C.!D.(C | D --> C))"
oops

I understand that it's open in FOL, but ultimately we're not in FOL,
we're in Isabelle/HOL, and because of this thread and the related
thread, I now consider that I'm mixing propositional logic with
first-order logic. Actually, I now consider that any FOL closed formula
can be considered an atomic formula in propositional logic.

Am I right or wrong? I'm think I'm right enough, and I explain a little
below.

Now, propositional logic is just a sublogic of first-order logic, with no
function symbols and where all predicate symbols have arity zero.

That's the traditional view.

But Isabelle/HOL is not traditional mathematics. It's not propositional
logic and it's not first-order logic.

I now depart from the traditional view, and I now consider, as I
mentioned, that FOL sentences (closed formulas, formulas with no free
variables), qualify as propositional atomic formulas (atomic sentences).

(At this point, it is entirely possible that I'm completely confused,
and that I'm repeating what you're already saying.)

You're generalizing so that propositional logic is also first-order
logic.
On the other hand, I'm generalizing a certain class of FOL
formulas, the closed formulas, so that they are also atomic sentences in
propositional logic.

Atomic sentences merely need be a string of symbols in which I can
definitely say the sentences are either true or false. In Isabelle/HOL,
every FOL closed formula is either true or false (can I be wrong on such
a basic idea?).

Bilaniuk says on page 3,

"Definition 1.1 item (3): Atomic formulas: A_0,..."

"Definition 1.2 item (1): Every atomic formula is a formula."

"The atomic formulas, A_0, A_1, ..., are meant to represent
statements that
cannot be broken down any further using our connectives, ...'".

Unlike with first-order atomic formulas, I am free to say what my
proposition atomic formulas are, as long as they can be interpreted as
either true or false (wrong again? considering FOL 0-ary predicates?).

The formal development of propositional logic, per Bilaniuk's Definition
1.1 and Definition 1.2, page 3, is completely independent of the formal
development of first-order logic, per Definitions 5.1, 5.2, and 5.3,
pages 24, 26, and 27.

I don't even try to figure out how Bilaniuk's first-order logic
definition could be rephrased to use Definitions 1.1 and 1.2, because
that's not what I want.

(Here, I go back and study your last sentence above, rather than just
blow by it.

Definition 5.1 item (5) of Bilaniuk requires that any FOL language
include the "=" primitive, not to mention the quantifier symbol.
Definition 1.1 doesn't require that a language of propositional logic
have these symbols, so not every language of propositional logic
qualifies as a first-order language.

However, suppose we ignore "=" and "forall" when they're not used. This
gets into my pet peeve about people making the FOL specification
synonymous with a "locked in, defined" language of first-order logic per
the requirement of the FOL specification.

I now extend my pet peeve to the "propositional logic specification" not
being synonymous with a "locked in, defined" language of propositional
logic, where the differences between two languages would be their
specific atomic formulas of Definition 1.1 item (3).

So, how can we assume anything if we haven't stated specifically both
our language of propositional logic and our language of first-order logic?

Okay, I look at the FOL specification again, and it might allow for an
infinite number of predicate symbols, so possibly we could define a FOL
language which contains every other FOL language, and likewise for a
"most generalized" language of propositional logic. That's not my
application, and, by text, I can't thoroughly interrogate you on these
kind of things.

I stop here on this. Writing what I write won't likely get read, so
writing two times the amount is even less likely to get read.)

The "variables" here are just predicates. Thus, it is
enough to fix an interpretation for these predicates in
order to have the definite truth-value of the expression. So, from
this point of view, every well-formed expression in propositional logic is
a assertion, i.e., a sentence. That is why,
I think, it can be called propositional or sentential logic.

I think we ended up at the same point; but possibly not. I decided that
the complete formula of my (3) above qualified as propositional logic,
but not as first-order logic.

But it comes back to emphasis. I think you're analyzing the formula of
(3) independent of "theorem", and I was analyzing as part of the Isar
command theorem "(A | B --> A) <-> (!C.!D.(C | D --> C))". So using
your terminology, the formula of (3) doesn't have single truth value
under all interpretations.

I am not sure if this view (as written above) is shared by other people,
though.

I'm sure that most everyone would have a view, but most everyone won't
have read this far, because involved technical discussions by text
aren't "workable".

You could straighten me out where I'm wrong, but getting completely
straightened out can never happen on an electronic forum. There is no
substitute for locally sitting under the masters, although I've had
plenty of local masters who didn't give me any time.

One more point for anyone listening. Any straightening out must be a
solution that's applicable to the masses, where the masses would be
people with a understanding of 1st and 2nd year university logic along
the lines of Rosen's Discrete Mathematics.

http://www.mhhe.com/math/advmath/rosenindex.mhtml

Isabelle requires a more sophisticated understanding of logic than that
level, but requiring too much beyond that will get Isabelle rejected by
the masses, or, better said, books about Isabelle beyond that will be
rejected by the masses.

I'm learning that I don't have to u
[message truncated]

Last updated: Apr 26 2024 at 20:16 UTC