#2, It's false to claim that (A V A) is a tautology unless A is a tautology
(A v A)<=> A, is tautologous.

(p->q & q) <-> q
[(p->q & q) -> p] <-> (q -> p)

(p->q & q) -> p, is invalid. It is false when p=F and q=T.
T T T T T
F T T F F
T F F T T
F F F T F

Tautologies are logical truths.
In virtue of truth tables (p & q) -> q is a tautology.
and
((p -> q) & p) <-> (p & q), is a tautology.
therefore
((p -> q) & p) -> q is a tautology.

1, x=y defined: E!x & E!y & (All F)(Fx <-> Fy).
and
2. E!x defined: (Some F)(Fx).

3. (All x)(x=x <-> E!x), is a theorem.
If either or both do not exist then x=y is provably false.

4. (All x)(x=x) is not valid.

example
(The present King if France)=(The present King if France), is false, even though
(All F)(F(The present King if France) <-> F(The present King if France)), is tautologous.

((P V Q) & (P -> ~R) & (Q -> ~R)) -> ~R, is tautologous.
T T T F T F F
F T F F T F F
T F T F F F F
F F F F F F F

Because ((P V Q) & (P -> ~R) & (Q -> ~R)) is a contradiction.

(P v Q) & ~P & ~Q, is a contradiction.
((T v T) & F & F) = F
((F v T) & T & F) = F
((T v F) & F & T) = F
((F v F) & T & T) = F.

1."A" is necessarily true iff "not-A -> (B and not-B)", is invalid.
It fails when "A" is necessarily true if "not-A -> (B and not-B)".

(not-A -> (B and not-B)) iff A, is a theorem.
(not-A -> (B and not-B)) iff necessary A, is not a theorem.

2. "A" is possible true iff "A or not-A" is true
A or -A, is true for all values of A. Possible A is false when a is A contradiction.

3. "A" is empirically true iff "A" is true.
False, 'B or not-B' is true and 'B or not-B' is not empirical.

It is false to say 'possible A' claims 'A or not A'.
It is false to say 'A or not A' is contingent.

'A or not A' is tautologous, necessarily true.

Not (The apple is red) <-> The apple is not red, is not valid.
It fails in the case of no apples...as you have noted.

(Not (The apple is red) <-> The apple is not red) <-> (the apple)exists, is valid.

Ep(p).

(All statements are false) is false, and it is equivalent to
(Some statements are true).

1. (All p)(~p) -> ~q.
2. (All p)(~p) -> ~(~q).
3. (All p)(~p) -> q.
4. (All p)(~p) -> (~q & q).
5. ~(All p)(~p).
6. (Some p)(p).

Also,
(All statement are true) is false, and it is equivalent to
(Some statements are false).

~E!(the x: Fx & ~Fx).

"For "Ga" to be a wff, doesn't a have to be an object in your domain of discourse?"

Vulcan rotates.
Pegasus flies.
Santa wears a red suit.
Etc. are false WFF where the subject terms do not exist.

"What sense can be made of asserting "Ga" if you don't already know that a exists?"

Pegasus exists, is a sensible wff that is false.

There are no true propositions that have non-referring names or non-referring descriptions as their subject.

Of course 'exists' is a predicate.
'a exists', has 'a' as its subject and 'exists' as its predicate.

But, exists is not a primary predicate.
(Ga & (a exists)) <-> Ga, ie. (a exists) does not add information to Ga.

If we define (a exists) as ∃F(Fa), and
(G exists) as ∃xGx.

1. |-. Ga -> ∃F(Fa). |-. Ga -> (a exists).
2. |-. Ga -> ∃x(Gx). |-. Ga -> (G exists).
3. |-. Ga -> ∃F∃x(Fx). |-. Ga -> ((Ga) exists).

(x exists) <-> ∃F(Fx).
(x exists) <-> ∃y(x=y).
(x exists) <-> x=x.
(x exists) <-> ((~F)x <-> ~(Fx)).

"Existence in the most general sense means being identical to oneself and different from others."

I agree that: x exists <-> x=x
x exists <-> Ey(x=y)

Names and descriptions refer or not.

1. (x=x, for all x) is an axiom in FOPL=.

Leibnitz/Russell: x=y =def AF(Fx <-> Fy).
In which case x=x <-> AF(Fx <-> Fx),
ie. x=x is tautologous for any x.

AF(F(Vulcan) <-> F(Vulcan)) is tautologous.
Therefore, Vulcan exists ???

Note that: AF(F(The present King of France) = F(The present King of France)), is also tautologous.
Therefore (The present King of France exists) ???

A better definition of Identity...
x=y =def (EF(Fx) & EF(Fy) & AF(Fx <-> Fy)).
x=x <-> (EF(Fx) & EF(Fx) & AF(Fx <-> Fx)).
x=x <-> EF(Fx).
x=x <-> x exists.

If x or y do not exist then x=y is false.

Srap Tasmaner...
Suppose I claim there is a smallest positive real number, call it k.
It's easily proven that k < 1, right?
Does that prove that there is a smallest positive real number?

No.
The name k is a non-referring description, like the present King of France.
There are no provable qualities of k.

If k exists then 1/k (the largest real number) must also exist, which is false.
There are no positive qualities of k that are true!

Naming or describing do not require reference.

Vulcan does not exist.
Pegasus does not exist.
Santa does not exist.
etc.

Sometimes naming does not bring things into existence.

HI Srap Tasmaner.

1. Ga -> ∃x(Gx), is valid.
2. Ga -> ∃F(Fa), is valid.
3. Ga -> ∃x∃F(Fx) is valid.

1 is 1st order and 2 and 3 are 2nd order theorems.

1a. Ga -> G exists.
2a. Ga -> a exists.
3a. Ga -> ((G exists) & (a exists)).

If it is true that unicorns have four legs then unicorns exist.
Truth is that which can be shown to be the case.
To show that 'Unicorns have four legs' is true, we need to verify it.
Verification requires the existence of unicorns and unicorn legs.

One truth about x proves x exists. ..where x is the subject of the truth.

Gx -> ∃F(Fx), is tautologous.

|-. Gx -> x exists.

noAxioms..

F is a variable predicate of individuals x

(some F)(Fx) means there is at least one instance of F such that Fx is true.
ie. Ax v Bx v Cx ...

Fx is true for a value of F.

If x has a predicate B, eg. (Bx),
and B is a value of F then (some F)(Fx).

Bx -> (Ax v Bx v Cx ...).

One truth about x proves x exists.

noAxioms...

x exists =def (some F)(Fx).
Descartes exists <-> (some F)(F(Descartes)).

If Descartes has a particular predicate such as 'thinks' (Descartes thinks) then
there is some predicate of Descartes that is true.

(Descartes thinks) implies (some F)(F(Descartes)).
This is an instance of the theorem: Ga -> (some F)(Fa), for any G.

Also..
If 'Descartes thinks' then the predicate 'thinks' exists.

1. Descartes thinks therefore Descartes exists.
2. Descartes exists therefore Possible(Descartes exists)
therefore,
3. Descartes thinks therefore Possible(Descartes exists).

By, ((p -> q) & (q -> r)) -> (p -> r).

Even with 'logical consistency' there is no omnipotent being.

We prove what does not exist by showing a logical contradiction, expressed as "P and not P, at the same time. eg: the ball is on fire and is not on fire at the same time. This is how we prove what is impossible.

The proposed gods of Christianity, Islam, Judaism are all claimed to be omnipotent. Omnipotent is to be able to do all things. We need to parse what omnipotent means, to be fair to the religious... to mean "able to do all possible things", because we know that god cannot do what is impossible.

It is possible to form a rock and it is possible to lift a rock. Can the omnipotent being form a rock that cannot be lifted? If yes, then the omnipotent being is not omnipotent (P and not P, at the same time) because it cannot lift the rock. If no, then the omnipotent being is not omnipotent because it cannot form the rock.

All logical options are covered, the answer to the question is either yes or no and either way it is impossible for that god to exist. If a god exists, and it is possible, then god is not omnipotent. This argument proves that the proposition "the Christian god exists" (or Muslim or Jewish) are false and not belief statements. Belief statements are not false anymore than they are true. No myth, assumption or opinion (the 3 belief types) are proven true or false. What is true or false is not a matter of belief.

'I think, therefore I'm possible' is a tautology.

1. I think, therefore I am.
Gx -> (some F)(Fx).

2. I am therefore It's possible that I am.
(some F)(Fx) -> possible((some F)(Fx)).

Therefore,

3. I think, therefore I'm possible.
Gx -> possible((some F)(Fx)).

Yes 'I think therefore I am' is an instance of the tautology: Gx -> EF(Fx), for all x.

'I think' has the form Gx. I am has the form EF(Fx).

If x has the predicate G then there is a predicate F such that x has that predicate, is tautologous.