Talk:Paraconsistent logic: Difference between revisions

Revision as of 02:33, 19 February 2017

Latest revision as of 08:08, 7 February 2024

(30 intermediate revisions by 8 users not shown)

Line 1:

{{WikiProject banner shell|class=B|

{{Maths rating|class=B|priority=Mid|field=foundations}}

{{WikiProject Philosophy|importance=mid|class=b|logic=yes}}

{{WikiProject Mathematics|priority=Mid}}

}}

{{Technical|date=September 2010}}

== Don't follow ==

Line 21 ⟶ 22:

== Removed some content from the "Motivation" section ==

I removed some content from the "Motivation" section on the ground that it seemed to me not particularly well-written, and involved material that is (or ought to be) covered more thoroughly in [[Liar paradox]] and [[Dialetheism]], both of which are prominently linked to. Feel free to integrate this material back into the article if you feel it would be an improvement. [[User:Dbtfz|<fontspan colorstyle="color:maroon;">dbtfz</fontspan>]][[User talk:Dbtfz|^{<fontspan colorstyle="color:slategray;">talk</fontspan>}]] 05:47, 25 February 2006 (UTC)

== Recent addition of material on direct logic ==

Line 261 ⟶ 262:

Below is a suggestion how to the following section more accurate and authoritative.

{{edit requestCOI|A}}

[[User:Prof. Carl Hewitt|Carl]] ([[User talk:Prof. Carl Hewitt|talk]]) 14:14, 26 August 2016 (UTC)

Line 268 ⟶ 269:

::Thanks. I cleaned up the remainder of the section since I don't have a conflict because it is not my work. Please make improvements.

::The correct reference for the applications section is the following:

:::Carl Hewitt. ''Formalizing common sense reasoning for scalable inconsistency-robust information coordination using Direct Logic Reasoning and the Actor Model.'' in Vol. 52 of Studies in Logic. College Publications. ISBN-10: {{ISBN |1848901593}}. 2015.

::[[User:Prof. Carl Hewitt|Carl]] ([[User talk:Prof. Carl Hewitt|talk]]) 17:14, 26 August 2016 (UTC)

:::Hi there. The changes in question seem to have been implemented, as per the comment above. Please note that, while citing yourself should be discussed on the talk page (as you have done), it is not necessary to place the edit request template, unless no other editors are working on the article. Regards, [[User:VB00|VB00]] ([[User talk:VB00|talk]]) 11:49, 1 January 2017 (UTC)

Line 287 ⟶ 288:

Each of these principles has been challenged.

One approach is to reject disjunction introduction but keep disjunctive syllogism and transitivity. In this approach, rules of [[natural deduction]] hold, except for [[disjunction introduction]] and [[excluded middle]]; moreover, inference A⊢B does not mean necessarily mean entailment A⇒B. Also, the following usual Boolean properties hold: [[double negation]] as well as [[associativity]], [[commutativity]], [[distributivity]], [[De Morgan's laws|De Morgan]], and [[idempotence]] inferences (for conjunction and disjunction). Furthermore, inconsistency-robust proof by contradiction holds for entailment (A⇒(B∧¬B))⊢¬B. [[Carl Hewitt]] favours this approach, claiming that having the usual Boolean inferences, [[Natural deduction]], [[Double negation elimination]], [[Rule of weakening|Weakening for inference]] (If ⊢A, then B⊢A), and inconsistency robust [[Proof by Contradiction]] are huge advantages in [[software engineering]].<ref name="commonsense">"Carl Hewitt. ''Formalizing common sense reasoning for scalable inconsistency-robust information coordination using Direct Logic Reasoning and the Actor Model.''" in Vol. 52 of Studies in Logic. College Publications. ISBN-10: {{ISBN |1848901593}}. 2015.</ref>

Another approach is to reject disjunctive syllogism. From the perspective of [[dialetheism]], it makes perfect sense that disjunctive syllogism should fail. The idea behind this syllogism is that, if ''¬ A'', then ''A'' is excluded and ''B'' can be inferred from ''A ∨ B''. However, if ''A'' may hold as well as ''¬ A'', then the argument for the inference is weakened.

Line 306 ⟶ 307:

|}

Both reductio ad absurdum and the rule of weakening have been challenged in this respect, but without much success. Double negation elimination is challenged, but for unrelated reasons. By removing it alone, while upholding the other two one may still be able to prove all negative propositions from a contradiction. <!-- Template:Unsigned --><small class="autosigned">—&nbsp;Preceding [[Wikipedia:Signatures|unsigned]] comment added by [[User:Prof. Carl Hewitt|Prof. Carl Hewitt]] ([[User talk:Prof. Carl Hewitt#top|talk]] • [[Special:Contributions/Prof. Carl Hewitt|contribs]]) 20:53, 24 August 2016 (UTC)</small>

{{reflist talk}}

== I think there is a typo ==

Shouldn't the line that reads "Furthermore, inconsistency-robust proof by contradiction holds for entailment (A⇒(B∧¬B))⊢¬B." be "(A⇒(B∧¬B))⊢¬A"? <!-- Template:Unsigned IP --><small class="autosigned">—&nbsp;Preceding [[Wikipedia:Signatures|unsigned]] comment added by [[Special:Contributions/2601:602:200:DD1D:45C:20C:ECA5:624B|2601:602:200:DD1D:45C:20C:ECA5:624B]] ([[User talk:2601:602:200:DD1D:45C:20C:ECA5:624B#top|talk]]) 02:33, 19 February 2017 (UTC)</small>

== Outline of completeness proof and needed axiom schemas ==

Regarding the system of [[Paraconsistent logic#An ideal three-valued paraconsistent logic]], it appears to me that it should be possible to select 35 or fewer axiom schemas (the axioms being tautologies of paraconsistent logic) from which one could prove (using modus ponens) any tautology of paraconsistent logic (and not prove any other formulas). Given propositions ''P'' and ''F'', one can define what it means for ''P'' to be ''t'' (true only, not-false), ''b'' (both true and false, not-sharp), or ''f'' (false only, not-true) as follows:

:<math>\lnot P \to F</math> is true (''t'' or ''b'') iff either ''P'' is ''t'' or ''F'' is true;

:<math>((P \land \lnot P) \to F) \to F</math> is true iff either ''P'' is ''b'' or ''F'' is true; and

:<math>P \to F</math> is true iff either ''P'' is ''f'' or ''F'' is true.

See [[implicational propositional calculus#Completeness]] for an example of how a completeness proof works for a much simpler system. As in that case, two axiom schemas would be used here to get the [[deduction theorem]].

The completeness proof would follow the process by which one evaluates whether a formula ''F'' is a tautology. For each valuation, one calculates (by induction on the length of subformulas) the value of each subformula. For example, when ''P'' is ''t'' and ''Q'' is ''b'' so that ''P''→''Q'' is ''b'', we would need a theorem of the form

:<math>(\lnot P \to F) \to ((((Q \land \lnot Q) \to F) \to F) \to ((((P \to Q) \land \lnot (P \to Q)) \to F) \to F))</math>.

This might require upto 3 (for negation) plus 9 (for implication) plus 9 (for disjunction) plus 9 (for conjunction) axiom schemas (3+9+9+9=30).

After one finishes that induction reaching the full formula ''F'', we should have one of the following for each valuation:

:<math>\lnot F \to F</math> if the value of ''F'' is ''t'' for this valuation;

:<math>((F \land \lnot F) \to F) \to F</math> if the value of ''F'' is ''b'' for this valuation; or

:<math>F \to F</math> if the value of ''F'' is ''f'' for this valuation.

If ''F'' is indeed a tautology, then we should be in either the first or second case (not the third case). So now we need two more axiom schemas:

:<math>(\lnot F \to F) \to F</math>; and

:<math>(((F \land \lnot F) \to F) \to F) \to F</math>.

At this point we should have that ''F'' can be deduced from a sequence of hypotheses describing the valuation. Now we do a backward induction to remove the hypotheses by combining the different cases. If ''P'' is one of the propositional variables in ''F'', then we would use the deduction theorem to remove it from the left side of the sequents and put it on the right side as an hypothesis.

:<math>(\lnot P \to F) \to F</math>;

:<math>(((P \land \lnot P) \to F) \to F) \to F</math>; and

:<math>(P \to F) \to F</math>.

So now we use one axiom schema of the form:

:<math>((\lnot P \to F) \to F) \to (((((P \land \lnot P) \to F) \to F) \to F) \to (((P \to F) \to F) \to F))</math>.

This then gives us that ''F'' can be deduced from a shorted valuation which excludes ''P''. When this downward induction is finished, we will have an unconditional proof of ''F'' alone.

So we might (in the worst case) need 2 (for deduction) plus 30 (for construction) plus two (for getting ''F'' itself) plus one (for removing hypotheses). Total axiom schemas needed 2+30+2+1=35. [[User:JRSpriggs|JRSpriggs]] ([[User talk:JRSpriggs|talk]]) 04:27, 29 August 2018 (UTC)

Although all those 35 axiom schemas are tautologies of paraconsistent logic, they are not especially convenient as axioms. They are non-intuitive and mostly too specialized to be useful for general proofs. So we should try to replace them with shorter more general and intuitive axioms. For example, instead of using

:<math>(((F \land \lnot F) \to F) \to F) \to F</math>

to go from

:<math>((F \land \lnot F) \to F) \to F</math>

to ''F'', we could use conjunction elimination

:<math>(P \land Q) \to P</math>

to get

:<math>(F \land \lnot F) \to F</math>

and then apply

:<math>((F \land \lnot F) \to F) \to F</math>

to that to get ''F''. Also instead of having three axiom schemas to get from an hypothesis being ''f'' to the implication being ''t'', we could use just one

:<math>(P \to F) \to (\lnot (P \to Q) \to F)</math>.

Or we could go even further and use

:<math>\lnot (P \to Q) \to P</math>

followed by

:<math>(P \to Q) \to ((Q \to R) \to (P \to R))</math> (from the deduction theorem).

[[User:JRSpriggs|JRSpriggs]] ([[User talk:JRSpriggs|talk]]) 01:29, 30 August 2018 (UTC)

I was able to reduce it to twenty (20) axiom schemas which I listed at [[Paraconsistent logic#Included]]. Most of them are simpler (and thus potentially more useful) than they might have been. [[User:JRSpriggs|JRSpriggs]] ([[User talk:JRSpriggs|talk]]) 02:00, 31 August 2018 (UTC)

=== Illustrating the use of the axiom schemas by proving selected theorems ===

* to prove <math>(\lnot P \to P) \to P</math>

:<math>(P \to ((Q \to P) \to P)) \to ((P \to (Q \to P)) \to (P \to P))</math> axiom 2

:<math>P \to ((Q \to P) \to P)</math> axiom 1

:<math>(P \to (Q \to P)) \to (P \to P)</math> modus ponens

:<math>P \to (Q \to P)</math> axiom 1

:<math>P \to P</math> modus ponens

:<math>(P \to P) \to ((\lnot P \to P) \to P)</math> axiom 20

:<math>(\lnot P \to P) \to P</math> modus ponens QED

* to prove <math>((P \to Q) \to P) \to P</math> [[Peirce's law]]

:<math>\lnot (P \to Q) \to P</math> axiom 3

::<math>(P \to Q) \to P</math> hypothesis

::<math>((P \to Q) \to P) \to ((\lnot (P \to Q) \to P) \to P)</math> axiom 20

::<math>(\lnot (P \to Q) \to P) \to P</math> modus ponens

::<math>P</math> modus ponens

:<math>((P \to Q) \to P) \to P</math> deduction QED

* to prove <math>P \lor \lnot P</math> the [[law of excluded middle]]

:<math>(P \to (P \lor \lnot P)) \to (((\lnot P \to (P \lor \lnot P)) \to (P \lor \lnot P))</math> axiom 20

:<math>P \to (P \lor \lnot P)</math> axiom 8

:<math>(\lnot P \to (P \lor \lnot P)) \to (P \lor \lnot P)</math> modus ponens

:<math>\lnot P \to (P \lor \lnot P)</math> axiom 9

:<math>P \lor \lnot P</math> modus ponens QED

* to prove <math>\lnot (P \land \lnot P)</math> the [[law of noncontradiction]]

:<math>(\lnot P \to \lnot (P \land \lnot P)) \to ((\lnot \lnot P \to \lnot (P \land \lnot P)) \to \lnot (P \land \lnot P))</math> axiom 20

:<math>\lnot P \to \lnot (P \land \lnot P)</math> axiom 16

:<math>(\lnot \lnot P \to \lnot (P \land \lnot P)) \to \lnot (P \land \lnot P)</math> modus ponens

:<math>\lnot \lnot P \to \lnot (P \land \lnot P)</math> axiom 17

:<math>\lnot (P \land \lnot P)</math> modus ponens QED

* to prove <math>(\lnot P \to Q) \to (P \lor Q)</math> the [[converse (logic)|converse]] of [[disjunctive syllogism]]

:<math>(P \to (P \lor Q)) \to ((\lnot P \to (P \lor Q)) \to (P \lor Q))</math> axiom 20

:<math>P \to (P \lor Q)</math> axiom 8

:<math>(\lnot P \to (P \lor Q)) \to (P \lor Q)</math> modus ponens

::<math>\lnot P \to Q</math> hypothesis

::<math>Q \to (P \lor Q)</math> axiom 9

:::<math>\lnot P</math> hypothesis

:::<math>Q</math> modus ponens

:::<math>P \lor Q</math> modus ponens

::<math>\lnot P \to (P \lor Q)</math> deduction

::<math>P \lor Q</math> modus ponens

:<math>(\lnot P \to Q) \to (P \lor Q)</math> deduction QED

== When and how paraconsistent logic might be used ==

Suppose we are given a question in the form "''Given data &Gamma;, does condition &Delta; hold?''" where &Gamma; and &Delta; maybe compound propositions composed from atomic propositions using the logical connectives ''not'', ''implies'', ''or'', and ''and''.

In classical logic, we might proceed by testing whether &Gamma;→&Delta; is a tautology (of classical logic) and whether &Gamma;→~&Delta; is a tautology. If neither is a tautology, then there is insufficient data. If &Gamma;→&Delta; is a tautology and &Gamma;→~&Delta; is not, then the answer is ''yes''. If &Gamma;→&Delta; is not a tautology but &Gamma;→~&Delta; is, then the answer is ''no''. If both are tautologies, then the data is inconsistent and no conclusion can be drawn unless the data is modified (perhaps by deleting some parts).

If we have paraconsistent logic available, then we could re-evaluate the inconsistent case by asking the same questions with respect to tautologies of paraconsistent logic. If neither is a tautology of paraconsistent logic, then there is insufficient ''relevant'' data. If &Gamma;→&Delta; is a tautology and &Gamma;→~&Delta; is not, then the answer is ''yes''. If &Gamma;→&Delta; is not a tautology but &Gamma;→~&Delta; is, then the answer is ''no''. If both are tautologies of paraconsistent logic, then even the relevant data is inconsistent and we are still stumped. [[User:JRSpriggs|JRSpriggs]] ([[User talk:JRSpriggs|talk]]) 05:38, 9 September 2018 (UTC)

== Translation of classical logic into paraconsistent logic ==

See [[Double-negation translation]]. Following this idea to translate classical logic into paraconsisent logic will show that paraconsistent logic's expressive power is not fundamentally inferior to that of classical logic. Reserve a propositional atom ''p''₀ to play the role of falsity. Then the translation is done as follows:

* Any propositional atom ''p''_''n'' for ''n'' ≥ 1 will be translated as (''p''_''n'' → ''p''₀) → ''p''₀ which is classically equivalent to ''p''_''n'' v ''p''₀.

* If ''P'' is any proposition of classical logic whose translation is ''Q'', then the translation of ~''P'' is ''Q'' → ''p''₀ which is classically equivalent to ~''P'' v ''p''₀.

* If ''P'' translates to ''Q'' and ''R'' translates to ''S'', then ''P'' → ''R'' translates to ''Q'' → ''S'' which is classically equivalent to (''P'' → ''R'') v ''p''₀. [From this we get that modus ponens carries over to the translated formulas.]

* If ''P'' translates to ''Q'' and ''R'' translates to ''S'', then ''P'' v ''R'' translates to ''Q'' v ''S'' which is classically equivalent to (''P'' v ''R'') v ''p''₀.

* If ''P'' translates to ''Q'' and ''R'' translates to ''S'', then ''P'' & ''R'' translates to ''Q'' & ''S'' which is classically equivalent to (''P'' & ''R'') v ''p''₀.

Then if ''P'' (which does not contain ''p''₀) translates to ''Q'', ''P'' will be a tautology of classical logic if and only if ''Q'' is a tautology of paraconsistent logic. If ''p''₀ has the value ''t'' or ''b'', then the translation of any subformula of ''P'' will also have either the value ''t'' or ''b'' regardless of what the valuation does to the other propositional atoms. If ''p''₀ has the value ''f'', then the translation of any subformula of ''P'' will have either the value ''t'' or ''f'' and that value will be the same as the classical value of the (untranslated) subformula under the valuation which results by collapsing ''b'' into ''t''.

What makes this work is that we have avoided having "~" in the translation. If ''p''₀ has the value ''t'', then ''t'' → ''t'' = ''t'' which is fine whereas ~''t'' = ''f'' which would screw things up since this case is supposed to always have the value ''t'' and thus not affect whether the translation is a tautology or not. [[User:JRSpriggs|JRSpriggs]] ([[User talk:JRSpriggs|talk]]) 05:36, 14 September 2018 (UTC)

Another translation leaves the propositional atoms unchanged, adding a disjunction with ''p''₀ on the outside instead. For example,

:<math>(\lnot P \to \lnot Q) \to (Q \to P)</math>

is a classical tautology, but not a paraconsistent tautology. It could be translated to

:<math>(((P \to R) \to (Q \to R)) \to (Q \to P)) \lor R</math>

which is both a classical tautology and a paraconsistent tautology (generalizing here from ''p''₀ to ''R''). To see that modus ponens carries over for this version of translation, we need

:<math>((P \to Q) \lor R) \to ((P \lor R) \to (Q \lor R))</math>

to be a paraconsistent tautology which it is. [[User:JRSpriggs|JRSpriggs]] ([[User talk:JRSpriggs|talk]]) 20:37, 14 September 2018 (UTC)

== Variations on the connectives ==

Disjunctive syllogism fails since the classical tautology

:<math>(\lnot P \land (P \lor Q)) \to Q</math>

is not a paraconsistent tautology. This occurs even though

:<math>P = f</math> and <math>Q = t</math>

is the obvious solution of the left-hand side in classical logic with no explosion occurring.

This suggests that perhaps a stronger version of disjunction should be used. We could define "strong disjunction" as

:<math>(P \lor_s Q) = ((\lnot P \to Q) \land (\lnot Q \to P))</math>.

This differs from the original disjunction in that

:<math>(b \lor_s f) = (f \lor_s b) = f</math> rather than <math>(b \lor f) = (f \lor b) = b</math>.

If the classical disjunction is translated this way, then disjunctive syllogism would work because

:<math>(\lnot P \land (P \lor_s Q)) \to Q</math>

''is'' a paraconsistent tautology. However, this comes at a cost since

:<math>P \to (P \lor_s Q)</math> and <math>Q \to (P \lor_s Q)</math>

would not be paraconsistent tautologies.

It is also possible to define "weak disjunction" by

:<math>(P \lor_w Q) = (P \lor Q \lor \lnot (P \to Q) \lor \lnot (Q \to P))</math>

:<math>(b \lor_w f) = (f \lor_w b) = t</math>

although I find it hard to imagine a use for this.

Similarly, "strong conjunction" is

:<math>(P \land_s Q) = (P \land Q \land (\lnot P \to \lnot Q) \land (\lnot Q \to \lnot P))</math>

:<math>(b \land_s t) = (t \land_s b) = f</math>.

And "weak conjunction" is

:<math>(P \land_w Q) = (\lnot (P \to \lnot Q) \lor \lnot (Q \to \lnot P))</math>

:<math>(b \land_w t) = (t \land_w b) = t</math>.

One could define "strong implication" as

:<math>(P \to_s Q) = ((P \to Q) \land (\lnot Q \to \lnot P))</math>

:<math>(t \to_s b) = f</math>.

This would restore contrapositive, but at the cost of losing the deduction metatheorem (or making it more complicated since you would have to prove both directions).

A "weak implication" might be

:<math>(P \to_w Q) = ((\lnot P) \lor Q)</math>

:<math>(b \to_w f) = b</math>.

which would fail to satisfy modus ponens. Or one could go even further and define "very weak implication" as

:<math>(P \to_{ww} Q) = ((\lnot P) \lor_w Q)</math>

:<math>(t \to_{ww} b) = (b \to_{ww} f) = t</math>.

Although, once again I cannot imagine what use they might be. [[User:JRSpriggs|JRSpriggs]] ([[User talk:JRSpriggs|talk]]) 01:02, 25 September 2018 (UTC)

By induction, we can define the strongest (most often ''f'') reasonable interpretation of a classical formula and the weakest (most often ''t'') reasonable interpretation as follows:

:<math>S (p_k) = W (p_k) = p_k</math> atoms are unchanged

:<math>S (\lnot P) = \lnot W (P)</math>

:<math>W (\lnot P) = \lnot S (P)</math>

:<math>S (P \to Q) = (W (P)) \to_s (S (Q))</math>

:<math>W (P \to Q) = (S (P)) \to_{ww} (W (Q))</math>

:<math>S (P \lor Q) = S (P) \lor_s S (Q)</math>

:<math>W (P \lor Q) = W (P) \lor_w W (Q)</math>

:<math>S (P \land Q) = S (P) \land_s S (Q)</math>

:<math>W (P \land Q) = W (P) \land_w W (Q)</math>.

Conjecture: If <math>\lnot \Gamma</math> is ''not'' a classical tautology (that is, &Gamma; is not a contradiction) and <math>\Gamma \to \Delta</math> is a classical tautology, then

:<math>S (\Gamma) \to W (\Delta)</math>

is a paraconsistent tautology. [[User:JRSpriggs|JRSpriggs]] ([[User talk:JRSpriggs|talk]]) 18:44, 26 September 2018 (UTC)

== Need a plain English example - Badly ==

This article is not helpful to the average user who is not schooled in Logic symbols. We should give an example, or a couple of examples, in plain English without the use of symbols. [[User:Ileanadu|Ileanadu]] ([[User talk:Ileanadu|talk]]) 16:59, 1 November 2018 (UTC)

:The feature of classical logic which supporters of paraconsistent logic are trying to avoid could be illustrated by "''You do not have a pet dog. If you have a pet dog, then the Moon is made of green cheese.''". [[User:JRSpriggs|JRSpriggs]] ([[User talk:JRSpriggs|talk]]) 17:48, 1 November 2018 (UTC)

:The point is that from a false statement (such as a contradiction), one can (in classical logic) deduce ''anything'' including statements which are irrelevant and absurd. Some people are uncomfortable with this, especially if they want to be able to entertain contradictions, so they invented paraconsistent logic to get around it. [[User:JRSpriggs|JRSpriggs]] ([[User talk:JRSpriggs|talk]]) 19:00, 2 November 2018 (UTC)

== Clarification ==

The first line of this article seems contradictory, at least if you see it in this way:

A paraconsistent logic cannot be a subfield of logic that tolerates contradictions but at the same time deals with them in a "discriminating way". Orther it tolerates them or discrminates them. I think your first sentence should say, "a non-discriminating way" instead.

== A typo? ==

In the implication table (<math>P \Rightarrow Q</math>) in the section https://en.wikipedia.org/wiki/Paraconsistent_logic#An_ideal_three-valued_paraconsistent_logic, shouldn't the <math>b \Rightarrow f</math> cell be <math>b</math>? Isn't it the case:

<math>(V(P,0) \text{ and } V(P,1)) \Rightarrow V(Q,0) \quad\Leftrightarrow\quad

(V(P,0) \Rightarrow V(Q,0)) \text{ and } (V(P,1) \Rightarrow V(Q,0))</math>

[[User:Sofviic|Sofviic]] ([[User talk:Sofviic|talk]]) 19:25, 11 November 2021 (UTC)

:No. If you read the subsection on [[Paraconsistent logic#Strategy]], you will see why it has to be what it is. You are implicitly assuming a certain relationship between classical logic and paraconsistent logic. But that assumption renders paraconsistent logic virtually useless. [[User:JRSpriggs|JRSpriggs]] ([[User talk:JRSpriggs|talk]]) 23:31, 11 November 2021 (UTC)

::Ah! I see that now. Should we add a small caption near to the table that says something similar to "<math>b \Rightarrow f</math> has to evaluate to <math>f</math>; explained further down in [[Paraconsistent logic#Strategy]]"?

:::If you do, then please put it in a comment which can only be read by those editing the article. Otherwise you are cluttering up the section to cater to people who might otherwise give it an erroneous interpretation. [[User:JRSpriggs|JRSpriggs]] ([[User talk:JRSpriggs|talk]]) 23:07, 12 November 2021 (UTC)