I have a few questions about Formalization & Pseudo-code

[CGandC]

Hello, I have a few questions and I'd appreciate if you can please help me.

1. If I want to say "for every $i \in \Bbb N$ and $0 \leq j \leq i$ define $A_{i,j} := i$ and $B_{i,j} := i \cdot j$ ",
then is the logical formula used for this is as such?:
$\forall i \in \Bbb N. \forall ~ 0 \leq j \leq i. ~ \exists A_{i,j}. \exists B_{i,j}.( A_{i,j} = i ~\land ~ B_{i,j} = i \cdot j )$

2. Suppose we have the function $f: \Bbb Q \to \Bbb N$ defined as follows: for every $q \in \Bbb Q$ there exist $a \in \Bbb Z$ and $b \in \Bbb N^+$ s.t. $q = \frac{a}{b}$ and $q$ is a rational in its reduced form; then $f(q) = f(\frac{a}{b}) = |a| + |b|$.
Can this whole sentence be written as the following logical formula?:
$\exists f: \Bbb Q \to \Bbb N . \forall q \in \Bbb Q. \exists a \in \Bbb Z. \exists b \in \Bbb N^+ . ( q = \frac{a}{b} ~ \land ~ \text{ q is in reduced form } ). f(q) = f(\frac{a}{b}) = |a| + |b|$

3. Would the following pseudo-code be correct for describing both logical formulas above? define logical_formula(i,j): if j <= i: A_ij = i B_ij = i*j return A_ij , B_ij else: return True ## returning "True" because the formula is vacuously true in this case. ####################################################################################### define f(q): if is_rational(q) == True : a,b = find_reduced_form(q) return (|a| + |b|) else: return True ## returning "True" because the logical formula of the function definition ## is vacuously true in this case.

Thanks in advance for any help!

 

[mfb]

The existence of these numbers is trivial. I assume j is also a natural number (you should specify that): If you want to define A,B I would write
Define $A_{i,j} := i$ and $B_{i,j}:=i \cdot j \quad \forall i,j \in \Bbb N$ where $j\leq i$.
>=0 is trivial.
There is nothing wrong with English words in a definition. (2) is readable but the previous definition is easier to read.

Pseudocode that either returns an integer (or a pair of integers) or True is strange.

 

[CGandC]

Thanks!.
In addition, what is the difference between a function and a logical formula with a universal quantifier as its first quantifier ( when reading from left to right )?
for example, when I wrote the logical formula
$\forall i \in \Bbb N. \forall ~ 0 \leq j \leq i. ~ \exists A_{i,j}. \exists B_{i,j}.( A_{i,j} = i ~\land ~ B_{i,j} = i \cdot j )$
It means It'll output me different mathematical objects for instantiated $i,j$, as such:

instantiate $i=0,j=0$ and we get as an output : $A_{0,0} , B_{0,0}$
instantiate $i=1,j=0$ and we get as an output : $A_{1,0} , B_{1,0}$
instantiate $i=1,j=1$ and we get as an output : $A_{1,1} , B_{1,1}$
instantiate $i=2,j=0$ and we get as an output : $A_{2,0} , B_{2,0}$
$\vdots$


But I could also define a function that takes two numbers ( meaning, the function receives an ordered pair ) which are those same $i,j$ and outputs two numbers which are $A_{i,j} , B_{i,j}$ ( as ordered pair ), so what is the difference between defining such a function and a logical formula such as the one I've written above?

 

[SSequence]

I am not fully acquainted with (elementary) formal logic or anything, but I think there are few aspects here. Let's look at the first example. First of all, I assume that you want $j$ to be a natural number too. Now if you are trying to communicate then the best way would be to write the definitions in semi-formal way as in post#2.

Now let's first go through the outer quantifiers in your first example. You wrote along the lines of:
$\forall \, i \in \mathbb{N} \,\, \forall \, 0 \leq j \leq i \,\,(...)$
A few points that were already mentioned in post#2. The first one is that $0 \leq j$ is redundant if we already know $j$ to be a natural number. Secondly, due to the condition of $j \leq i$ being added just after the quantifier, the mention of $j \in \mathbb{N}$ has been missed.

Generically, one can proceed in a number of ways:
(1) It doesn't seem to me that this solution applies here, but it is worth mentioning since it does help in some circumstances. If you know that the statement you write is going to involve only natural numbers, then it is reasonable to explicitly mention before-hand that the quantification is implicitly assumed to be over natural numbers and then write:
$\forall \, i \,\, \forall \, j \leq i \,\,(...)$

As one other example (which I just made up), consider the statement:
$\forall \, x \in \mathbb{Z} \,\, \exists \, y \in \mathbb{Z}\,\,(x=y+1)$
As an alternate, we might as well mention before-hand that the quantification is assumed to be over $\mathbb{Z}$ and then write:
$\forall \, x \,\, \exists \, y\,\,(x=y+1)$

(2) You could write everything in a semi-formal way as mentioned in post#2. Normally, this would be the best option if the goal is clear communication.

(3) Another option is to write [which has some problems as mentioned at the beginning]:
$\forall \, i \in \mathbb{N} \,\, \forall \, j \leq i \,\,(...)$
as:
$\forall \, i \in \mathbb{N} \,\, \forall \, j \in \mathbb{N} \,\,(j \leq i \rightarrow (...))$

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

Some more points now. When we write something like:
$\forall i \in \Bbb N. \forall ~ 0 \leq j \leq i. ~ \exists A_{i,j}. \exists B_{i,j}.( A_{i,j} = i ~\land ~ B_{i,j} = i \cdot j )$
I think one other issue (if we are being formal) is similar to previous ones. Just writing $\exists A_{i,j}$, it is unclear what collection of objects this belongs to?

Instead of $A_{i,j}$, $B_{i,j}$, let me use total functions from $\mathbb{N}^2$ to $\mathbb{N}$ [I will assume you intend the entries to be well-defined for all input $i,j$]. Let $\mathcal {F}$ denote the collection of all total functions from $\mathbb{N}^2$ to $\mathbb{N}$ .

Now to assert the existence of a function which exactly corresponds to the array $A_{i,j}$'s entries (at the relevant places) we can write something like:
$\exists f \in \mathcal{F} \,\, \forall \, i \in \mathbb{N} \,\, \forall \, j \in \mathbb{N} \,\,(j \leq i \rightarrow (f(i,j)=i))$
Similarly to assert the existence of a function which exactly corresponds to the array $B_{i,j}$'s entries (at the relevant places) we can write something like:
$\exists f \in \mathcal{F} \,\, \forall \, i \in \mathbb{N} \,\, \forall \, j \in \mathbb{N} \,\,(j \leq i \rightarrow (f(i,j)=i \cdot j))$

 

[pbuk]

What are you actually trying to achieve here? If the end result is some program code or pseudocode then writing statements using the symbology of predicate logic isn't going to help; if the end result is a statement or proof in predicate logic then psuedocode isn't going to help.

 

[CGandC]

What are you actually trying to achieve here? If the end result is some program code or pseudocode then writing statements using the symbology of predicate logic isn't going to help; if the end result is a statement or proof in predicate logic then psuedocode isn't going to help.

I find the formal language of a proof or a mathematical definition to very much resemble pseudo-code so I was intrigued to see how one might translate the given logical formulas to computer code ( the logical formulas above could've been written better, but I wanted a general perspective to what the code might look like ).
Now that I think of it, there are couple of questions related to this:
1. Are there algorithms to make computer capable of "conjuring" up a mathematical proof? I know the answer is no because of a theory I don't understand yet that's called "Curry-Howard Correspondence "
2. can any kind of mathematical proof be translated into pseudo-code?
3. can any kind of statement written in predicate logic ( or other systems of logic ) be translated into pseudo-code?

I'm not sure about questions 2 & 3 ( when studying Algorithms you are enforced to translate descriptive steps into some sort of a structure that resembles pseudo-code. But on the other hand, Algorithms only compute or allow us to prove properties about some mathematical objects [ like proving if a number is prime or not ] , so I'm not if any proof can be translated into pseudo-code .) and the answer to these questions might change if in our proof there is a process that never ends ( for example when proving that every set whose cardinality is $\aleph_0$ has a proper-subset of cardinality $\aleph_0$ we involve an infinite process in the prove [ at least in the proof I've learned, I can write it if anyone's interested ] ), but I don't think such processes should bother us because we only want to translate the language of a proof ( or translating a logical formula ) into a pseudo-code.

 

[mfb]

Computers are already used to verify some proofs and they can come up with very simple proofs on their own.

There is ongoing work to convert mathematics to a computer-readable format, but people are still working on undergrad mathematics there.

Wikipedia has multiple articles about that topic:

https://en.wikipedia.org/wiki/Proof_assistant

https://en.wikipedia.org/wiki/Automated_theorem_proving

https://en.wikipedia.org/wiki/Metamath

And more.

 

[Stephen Tashi]

so what is the difference between defining such a function and a logical formula such as the one I've written above?

One version of this question is:

If (it is true that) $\forall x ( \exists y) P(x,y) )$ then does there (necessarily) exist a function $f$ such that $P(x, f(x))$ ? - where $P(x,y)$ is a given propositional function and where the domain and codomain of $f$ match the domains of $x$, $y$, $P(x,y)$..

As to writing such a quantified statement in pseudo-code, the term pseudo-code is ambiguous until a context is defined where the code executes some action. It seems to me that $\forall x ( \exists y) P(x,y) )$ leaves open the possibility that there might be two (or more) functions $f_1, f_2$ that satisfy $P(x,f_1(x))$ and $P(x, f_2(x))$. So I don't see how writing pseudo-code for only one such function $f$ portrays an equivalent statement.

 

[CGandC]

Very interesting information...

So I don't see how writing pseudo-code for only one such function $f$ portrays an equivalent statement.

we'd need to provide some universe for $x$ and $y$ , let's denote them as $U_1$ and $U_2$ write the logical formula as $\forall x \in U_1 ( \exists y \in U_2 ) P(x,y) )$. Then for the pseudo code, we'd write a process that takes an arbitrary element in $U_1$ and then we'd give a description as to how one would chose $y \in U_2$ such that $P(x,y)$ would evaluate to true. If we were to chose an arbitrary $x \in U_1$ we can write a recursive process that finds some function $f$ s.t. $P(x, f(x))$ and this methodology can be used for example in defining ( defining recursively ) sets of functions that satisfy a specific property ( which arises a lot when proving a property about a recursively defined set using a tool called 'structural induction' ).

Now, the pseudo-code might never terminate when viewed as written in a computer ( that's because we'd have to loop all $x$ values in $U_1$ and $U_1$ can be infinite, hence the pseudo-code may not be computable ) , but when written on paper it can be considered as legit ( like proving a theorem by induction, on paper the proof is considered legit but when attempted to write the proof in a computer, the proof will never terminate since there are infinite naturals ).

 

[Stephen Tashi]

So you are saying $\forall x ( \exists y P(x,y)$ is equivalent to asserting the existence of a function. i.e. $\exists f \ { \forall x ( P(x,f(x))}$.

 

[CGandC]

Sort of, I've elaborated my question below:
Let's look at the logical formula,
$( * ) ~~$, $\forall x \in U_a . \exists y \in U_b. P(x,y)$ and assume it is correct ( also assume $U_a , U_b \neq \emptyset$ ).
This means,
Take $u_1 \in U_a$ and instantiate it in $( * )$ then an element $y_1 \in U_b$ is "spurred" out in our environment ( our context we're currently working in ) .
Take $u_2 \in U_a$ and instantiate it in $( * )$ then an element $y_2 \in U_b$ is "spurred" out in our environment.
.
.
.
And more values in $U_b$ can be "spurred" out if we chose to instantiate objects from $U_a$ into $( * )$

So my question was: is it possible to take the formulas
$( * ) ~~$ $\forall x \in U_a. \exists y \in U_b. P(x,y)$
$( * ) ~~$ $\forall x \in U_a. \forall y \in U_b. P(x,y)$
and translate each of them into a mathematical function? and if so, how would one write it using predicate logic? ( I've written my attempt below )

The function may not be a specific rule ( like: $f(x) = x^2 , \forall x \in \Bbb R$ ) but it may be a procedure ( like when proving that every infinite set has an infinite subset of cardinality $\aleph_0$; a common proof of this involves a process with the usage of the axiom of choice ).

My attempt: ( Assume that $( * )$ and $( ** )$ are true )

$( * ) ~~$: Here I want to formulize the formula to a function that takes x values from $U_a$, along the way finds a value y from $U_b$ ,and will eventually spit out a logical formula $P(x,y)$ ,
$\forall x \in U_a . \exists y \in U_b . P(x,y) \iff \exists f: U_a \to U_b . \forall x \in U_a . \exists y \in U_b. f(x) = P(x,y)$ ( is this equivalence true? )

$( ** ) ~~$: Here I want to formalize the formula to a function that takes x values from $U_a$ and will spit out the logical formula $\forall y \in U_b . P(x,y)$ ,
$\forall x \in U_a. \forall y \in U_b. P(x,y) \iff \exists f: U_a \to U_b . \forall x \in U_a . \forall y \in U_b. f(x) = P(x,y)$ ( is this equivalence true? )

However, both attempts are incorrect because $f(x) = P(x,y)$ means that my function will spit out either True or False values, and I want it to return logical formula.

 

[SSequence]

...... ( like proving a theorem by induction, on paper the proof is considered legit but when attempted to write the proof in a computer, the proof will never terminate since there are infinite naturals ).

I think you are misunderstanding some aspects of the formalization of proofs. When people talk about (computer) formalization of proofs, the proofs are finite in length. Formalization of a proof isn't the same as exhaustive searching.
(Perhaps you weren't talking about formalization, in which case this isn't relevant)

Sort of, I've elaborated my question below:
Let's look at the logical formula,
$( * ) ~~$, $\forall x \in U_a . \exists y \in U_b. P(x,y)$ and assume it is correct ( also assume $U_a , U_b \neq \emptyset$ ).
This means,
Take $u_1 \in U_a$ and instantiate it in $( * )$ then an element $y_1 \in U_b$ is "spurred" out in our environment ( our context we're currently working in ) .
Take $u_2 \in U_a$ and instantiate it in $( * )$ then an element $y_2 \in U_b$ is "spurred" out in our environment.
.
.
.
And more values in $U_b$ can be "spurred" out if we chose to instantiate objects from $U_a$ into $( * )$

So my question was: is it possible to take the formulas
$( * ) ~~$ $\forall x \in U_a. \exists y \in U_b. P(x,y)$
$( * ) ~~$ $\forall x \in U_a. \forall y \in U_b. P(x,y)$
and translate each of them into a mathematical function? and if so, how would one write it using predicate logic? ( I've written my attempt below )

Replying to certain parts of the post. It seems that what you are doing is similar to how one would define function. I will write the set $U_a$ as $A$ and the set $U_b$ as $B$. So the way one would define a function (from $A$ to $B$) would be as a special kind of subset of $A \times B$.

From the perspective of sets, functions would be defined as a certain kind of relation $R$. For any specific set $R \subseteq A \times B$ [assuming $A,B \neq \phi$ to avoid vacuous boundary cases], we will have a predicate $P(x,y)$ such that for any arbitary $x \in A$ and $y \in B$ we will have $y=f(x)$ if and only if the predicate $P(x,y)$ is true. So we would be able to write the relation $R$ as:
$R=\{(x,y) \in A \times B \, | \, P(x,y) \}$

And now saying that:
"The relation $R$ is a function from $A$ to $B$."
is equivalent to the following:
$\forall x \in A \, \exists_{(=1)} \, y \in B \, [P(x,y)]$
$\forall x \in A \, \exists y \in B \, [P(x,y) \, \wedge \, \forall i \in B \, (P(x,i) \rightarrow i=y)]$

In set theory language $P(x,y)$ would be a predicate with free two variables, so it will have a truth value for any arbitrary combination of sets $x$ and $y$. However, when $x \in A$ and $y \in B$, the predicate $P(x,y)$ will be true exactly when $y=f(x)$.
Edit: Modified the ordering of the post a bit to make it easier to read.

 

[Stephen Tashi]

So my question was: is it possible to take the formulas
$( * ) ~~$ $\forall x \in U_a. \exists y \in U_b. P(x,y)$
$( * ) ~~$ $\forall x \in U_a. \forall y \in U_b. P(x,y)$
and translate each of them into a mathematical function?

I think "translate" isn't an appropriate word. If the logical expresses were mathematical functions in some language then it would make sense to speak of "translating" them to computer code. However, there is a distinction between propositions and propositional functions. For example (for real numbers) "$\forall x (x > x+1)$" is a proposition, which has the constant value "True". By contrast "$x > x + y$" is a propositional function because its truth value depends on what we use for $x$ and $y$. (A good rule of thumb is that an expression with an unquantified variable cannot be a proposition.)

If $\forall x \in U_a. \exists y \in U_b. P(x,y)$ is assumed to be a True proposition, then we can ask if this asserts the existence of a function $f$ such that $P(x,f(x))$ is True for all values of $x$. The abstract existence of such a function does not specify how to code it. How to code it would depend on the specifics of $P(x,y)$.

For example, a proposition such as $\forall x \exists y (y > x)$ does not imply a particular way of implementing a function $f$ such that the propositional function $P(x,f(x)$ takes the constant value True. For example, it doesn't imply that $f(x)$ must be $x+1$ or $x+7$ etc. So how are you visualizing that the function $f$ will be created? A human being can invent $f$. Is that what you are proposing?

(From the point of view of pure math, there might be technicalities involving The Axiom of Choice. But that would be a big digression from computer programming.)

The function may not be a specific rule ( like: $f(x) = x^2 , \forall x \in \Bbb R$ ) but it may be a procedure ( like when proving that every infinite set has an infinite subset of cardinality $\aleph_0$; a common proof of this involves a process with the usage of the axiom of choice ).

I'm not sure whether you envision yourself (as a human being) executing this procedure or whether you are thinking about a computer program that executes it.

If we know $\forall x \exists y P(x,y)$ is a True proposition then it is unnecessary to prove that proposition by doing an inductive (or other type of) proof.

So it seems to me that your question is whether the existence of a True proposition of a certain form implies the existence of a proof of that proposition. In particular, you are interested in a proof using the method "universal generalization". For example, using that method to prove $\forall x \ \exists y\ P(x,y)$ involves considering an "arbitrary" $x$ and showing an appropriate $y$ exists for it.

 

[CGandC]

"The relation $R$ is a function from $A$ to $B$."
is equivalent to the following:
$\forall x \in A \, \exists_{(=1)} \, y \in B \, [P(x,y)]$
$\forall x \in A \, \exists y \in B \, [P(x,y) \, \wedge \, \forall i \in B \, (P(x,i) \rightarrow i=y)]$

1. how common is it to encounter a set consisting of logical formulas? in what areas of mathematics? for example the following set:
$K = \{ ~( \forall x \in A. \forall y \in B. P(x,y) ) ~ , ~( \forall x \in A. \exists y \in B. P(x,y) ) ~ \}$

2. I can define a function $f: \{ 0,1 \} \to K$ as such:
$f(0) = ( \forall x \in A. \forall y \in B. P(x,y) ) ~$
$f(1) = ( \forall x \in A. \exists y \in B. P(x,y) ) ~$

Now, on the one hand , logical formulas which are True can be used to "spur" out mathematical objects, like here in my comment:

Let's look at the logical formula,
$( * ) ~~$, $\forall x \in U_a . \exists y \in U_b. P(x,y)$ and assume it is correct ( also assume $U_a , U_b \neq \emptyset$ ).
This means,
Take $u_1 \in U_a$ and instantiate it in $( * )$ then an element $y_1 \in U_b$ is "spurred" out in our environment ( our context we're currently working in ) .
Take $u_2 \in U_a$ and instantiate it in $( * )$ then an element $y_2 \in U_b$ is "spurred" out in our environment.
.
.
.
And more values in $U_b$ can be "spurred" out if we chose to instantiate objects from $U_a$ into $( * )$

On the other hand, since these logical formulas are True, then in the set $T$ I've wrote above,
if the logical formulas $~( \forall x \in A. \forall y \in B. P(x,y) ) ~ , ~( \forall x \in A. \exists y \in B. P(x,y) ) ~$ are true then does this mean that the set $T$ can be written as:
$T = \{ True, True \} = \{ True \}$ ?

So it seems to me that your question is whether the existence of a True proposition of a certain form implies the existence of a proof of that proposition.

3. Can a proof be viewed as a procedure that takes as an input the assumptions we make in the proof and this procedure then goes on to evaluate whether the theorem we are trying to prove is true or false?

Is that what you are proposing?

I was proposing if it is possible to define a function that takes an input and outputs a logical formula. ( such as the function $f: \{ 0,1 \} \to T$ I've described above)

 

[Stephen Tashi]

3. Can a proof be viewed as a procedure that takes as an input the assumptions we make in the proof and this procedure then goes on to evaluate whether the theorem we are trying to prove is true or false?

Essentially yes, but If a statement is proven false, it is not called a "theorem".

I was proposing if it is possible to define a function that takes an input and outputs a logical formula. ( such as the function $f: \{ 0,1 \} \to T$ I've described above)

You need to define what you mean by a "logical formula". Presumably you mean a symbolic expression representing a proposition.

In your example, you haven't defined a function that outputs "a logical formula", unless you consider the single result "True" to be a formula.

 

[CGandC]

a symbolic expression representing a proposition that is considered true, not only has the "True" value associated with it, but it also gives us a rule we could use in order to create mathematical objects or say things about existing object. What I mean is, take the following variant of the Archimedean Property for example: $\forall x \in \Bbb R . x > 0 \rightarrow \exists n \in \Bbb N . nx > 1$ . Not only that this symbolic expression representing a proposition is true, but also it provides us a rule that given any $x>0$ then the rule will provide us $n \in \Bbb N$ s.t. $nx > 1$.
So maybe this logical formula is equivalent to the ordered pair $\langle True , RULE \rangle$ where RULE is the rule of the logical formula.

So if we follow this mindset, If we have the set $K = \{ ~( \forall x \in A. \forall y \in B. P(x,y) ) ~ , ~( \forall x \in A. \exists y \in B. P(x,y) ) ~ \}$ where the symbolic expressions representing a proposition inside the set $K$ are all true, then we can associate an ordered pair with a truth value and a rule with each such true valued symbolic expression:
$~( \forall x \in A. \forall y \in B. P(x,y) ) ~ = \langle True, Rule_1 \rangle$
$~( \forall x \in A. \exists y \in B. P(x,y) ) ~ = \langle True, Rule_2 \rangle$
Then It is not true to say that $K = \{ True, True \} = \{ True \}$, but rather
$K = \{ \langle True, Rule_1 \rangle , \langle True, Rule_2 \rangle \}$

So, symbolic expressions representing a proposition that is true valued can be thought of as being an element in a relation , but the problematic point is that - if for example we look at $( \forall x \in A. \forall y \in B. P(x,y) ) = \langle True, Rule_1 \rangle$, then what can describe $Rule_1$? if it describes the same symbolic expression then we'd have :
$\langle True, Rule_1 \rangle = \langle True, ( \forall x \in A. \forall y \in B. P(x,y) ) \rangle = \langle True, \langle True, ( \forall x \in A. \forall y \in B. P(x,y) ) \rangle \rangle =...$

So you see the problem,
This is almost similar to the following:
If we treat the symbol $\in$ as being the element-hood relation then it'd be weird to claim that the formula $1 \in \Bbb N$ is a shortcut of writing $\langle 1 , \Bbb N \rangle ~ \in ~ \in$, which itself is a shortcut of writing $\langle \langle 1 , \Bbb N \rangle , \in \rangle ~ \in ~ \in$ , which itself is a shortcut of ... , and so on ( How does one solve this problem anyway? do we not define $\in$ as being a relation? ) .

 

[Stephen Tashi]

So, symbolic expressions representing a proposition that is true valued can be thought of as being an element in a relation , but the problematic point is that - if for example we look at $( \forall x \in A. \forall y \in B. P(x,y) ) = \langle True, Rule_1 \rangle$,

If you say a symbolic logical expression is but one element in a relation, why would we set a symbolic logical expression equal to an ordered pair of elements in that relation?

 

[CGandC]

What I was trying to say was - a logical expression is best thought of two objects,
one is the true/false value:
if the value is True, we associate with the logical expression an ordered pair as such : $\langle True , Rule_t \rangle$, where $Rule_t$ is the rule associated with the logical formula
if the value is False, we associate with the logical expression an ordered pair as such : $\langle False, Rule_f \rangle$ where $Rule_f$ is the rule associated with the negation of the false logical formula.

I was wrong at writing $( \forall x \in A. \forall y \in B. P(x,y) ) = \langle True, Rule_1 \rangle$ because it doesn't make sense at all, but looking at the idea of associating an ordered pair such as above to a logical formula , how would you one establish this association?

 

[Stephen Tashi]

What I was trying to say was - a logical expression is best thought of two objects,
one is the true/false value:

I think a "logical expression" is best defined as a set of symbols that obeys a certain syntax and has the semantics of representing a statement that is either True or False and not both (although the truth or falsity of it may not be known to the person writing it.)

If you want to deal only with logical expressions that have known truth values, I suggest you invent different terminology.

but looking at the idea of associating an ordered pair such as above to a logical formula , how would you one establish this association?

First, I would consider whether formalizing the notion of a logical expression with associated truth-value. is worthwhile for the purpose of answering the questions that are on your mind. Those questions need to be clarified. Is this going to be helped by defining notation and terminology for such a concept? Are you trying to create a data structure that would be used by a computer program?

 

[CGandC]

Good questions, I was just curious about how we might formalize correctly a set of logical expressions. I'll leave this curiosity aside for now, thanks for the help!