My Academia.edu Page w/ Publications

18 Jul 2018

Priest (11a.4) An Introduction to Non-Classical Logic, ‘Modal FDE,’ summary

 

by Corry Shores

 

[Search Blog Here. Index-tags are found on the bottom of the left column.]

 

[Central Entry Directory]

[Logic and Semantics, entry directory]

[Graham Priest, entry directory]

[Priest, Introduction to Non-Classical Logic, entry directory]

 

[The following is summary of Priest’s text, which is already written with maximum efficiency. Bracketed commentary and boldface are my own, unless otherwise noted. I do not have specialized training in this field, so please trust the original text over my summarization. I apologize for my typos and other unfortunate mistakes, because I have not finished proofreading, and I also have not finished learning all the basics of these logics.]

 

 

 

 

Summary of

 

Graham Priest

 

An Introduction to Non-Classical Logic: From If to Is

 

Part I:

Propositional Logic

 

11a

Appendix: Many-valued Modal Logics

 

11a.4

Modal FDE

 

 

 

 

Brief summary:

(11a.4.1) In our many-valued modal FDE logic, we have just the connectives ∧, ∨ and ¬, because A B is defined as ¬A B. (11a.4.2) FDE can be formulated as a four-valued logic, and the connectives can be evaluated with the following diamond lattice (Hasse diagram):

 

1

↗               ↖

b                                 n

↖                   ↗

0

 

f is the greatest lower bound;  f is the least upper bound; and f¬ maps 1 to 0, vice versa, and each of b and n to itself. (11a.4.3) Our modal FDE logic is called KFDE. “If we ignore the value n in the non-modal case (that is, we insist that formulas take one of the values in {1, b, 0}) we get the logic LP. In the modal case, we get KLP. If we ignore the value b in the non-modal case, we get the logic K3. In the modal case, we get KK3” (245). (11a.4.4) The equivalence between four-valued FDE truth-values and the four value-situations of the relational semantics are: v(A) = 1 iff Aρ1 and it is not the case that Aρ0 ; v(A) = b iff Aρ1 and Aρ0 ; v(A) = n iff it is not the case that Aρ1 and it is not the case that Aρ0 ; and v(A) = 0 iff it is not the case that Aρ1 and Aρ0 . The truth-falsity conditions for the connectives in the relational semantics are: A Bρ1 iff Aρ1 and Bρ1 ; A Bρ0 iff Aρ0 or Bρ0 ; A Bρ1 iff Aρ1 or Bρ1 ; A Bρ0 iff Aρ0 and Bρ0 ; ¬Aρ1 iff Aρ0 ; and ¬Aρ0 iff Aρ1 . “Validity is defined in terms of the preservation of relating to 1” (245). (11a.4.5) KFDE has the same relational semantics but with world designations and with the following rules for the necessity and possibility operators:

vw(A) = 1 iff Aρw1 and it is not the case that Aρw0

vw(A) = b iff Aρw1 and Aρw0

vw(A) = n iff it is not the case that Aρw1 and it is not the case that Aρw0

vw(A) = 0 iff it is not the case that Aρw1 and Aρw0

 

A Bρw1 iff Aρw1 and Bρw1

A Bρw0 iff Aρ0 or Bρw0

 

A Bρw1 iff Aρw1 or Bρw1

A Bρw0 iff Aρw0 and Bρw0

 

¬Aρw1 iff Aρw0

¬Aρw0 iff Aρw1

 

Aρw1 iff for all w′ such that wRw′, Aρw1

Aρw0 iff for some w′ such that wRw′, Aρw0

 

Aρw1 iff for some w′ such that wRw′, Aρw1

Aρw0 iff for all w′ such that wRw′, Aρw0

(based on with quotation from p.245-246)

(11a.4.6) Next Priest provides the argumentation for why the truth/falsity conditions are formulated the way they are. (11a.4.7) By adding a possible worlds exhaustion constraint to KFDE we can get KLP. (11a.4.8) By adding a possible worlds exclusion constraint to KFDE we can get KK3. (11a.4.9) By adding both the exhaustion and exclusion constraints to KFDE, we get the classical modal logic K. (11a.4.10) We can apply the world accessibility relation constraints (like ρ, σ, τ, etc) to our specific many-valued modal logics to get such extensions as: KFDEρ, KLPρτ, KK3σ and so forth. (11a.4.11) There are no logical truths (tautologies) in KFDE and KK3, because to be a logical truth means that the formula is true under all interpretations. But in KFDE and KK3, under any interpretation, every formula can be valued neither true nor false, and thus no formulas can be logical truths. (11a.4.12) The interpretations for the logics of the family we are considering are monotonic. (11a.4.13) A corollary of this is “that ⊨K A iff ⊨KLPA (and similarly for Kρ and KLPρ, etc.)” (247).

 

 

 

 

 

Contents

 

11a.4.1

[The Connectives in Our Many-Valued Modal FDE]

 

11a.4.2

[FDE as a Four-Valued Logic]

 

11a.4.3

[KFDE, KL, and KK3]

 

11a.4.4

[The Relational Semantics of FDE]

 

11a.4.5

[The Relational Semantics of KFDE]

 

11a.4.6

[The Rationale for the Modal Operator Truth/Falsity Conditions]

 

11a.4.7

[Obtaining KLP]

 

11a.4.8

[Obtaining KK3]

 

11a.4.9

[Obtaining K]

 

11a.4.10

[Extensions of Our Many-Valued Modal Logics]

 

11a.4.11

[The Lack of Logical Truths in KFDE and KK3.]

 

11a.4.12

[The Monotonicity of These Logics]

 

11a.4.13

[Corollary]

 

 

 

 

Summary

 

11a.4.1

[The Connectives in Our Many-Valued Modal FDE]

 

[In our many-valued modal FDE logic, we have just the connectives ∧, ∨ and ¬, because A B is defined as ¬A B.]

 

[Recall from section 11a.2 that we are formulating many-valued modal logics. We will now do a many-valued modal FDE logic. (See ch.8). Recall from section 8.2.1 that we have just the connectives ∧, ∨ and ¬, because A B is defined as ¬A B.]

Let us now look at one many-valued modal logic in more detail. The many-valued logic in question is FDE. The language for this has three connectives: ∧, ∨ and ¬. (Recall that A B is defined as ¬A B.)

(244)

[contents]

 

 

 

 

 

 

11a.4.2

[FDE as a Four-Valued Logic]

 

[FDE can be formulated as a four-valued logic, and the connectives can be evaluated with the following diamond lattice (Hasse diagram):

 

1

↗               ↖

b                                 n

↖                   ↗

0

 

f is the greatest lower bound;  f is the least upper bound; and f¬ maps 1 to 0, vice versa, and each of b and n to itself.]

 

[Recall from section 8.4 that we can formulate FDE as a four-valued logic (rather than as a two-valued logic with four truth-value situations enabled by a relational truth-value semantics; see section 8.2. In the four-valued version, the four values are: 1 (for just true), 0 (for just false), b (for both), and n (for neither), and the designated values are 1 and b. Next we should recall from section 8.4.3 how the diamond lattice works. Priest’s version is:

 

1

↗               ↖

b                                 n

↖                   ↗

0

 

I proposed something with more reminders in it for how it is read.

 

1

↙↗       

         ↖↘

b           

|

             n

        ↘↖        

         ↗↙

0

 

Negation toggles 0 and 1, and it maps n to itself and b to itself:

Negation and

1

↙↗       

        ↖↘

b           

|

             n

        ↘↖        

         ↗↙

0

 

Priest writes here that: “f¬ maps 1 to 0, vice versa, and each of b and n to itself”. For conjunction, we take the greatest lower bound for both of the conjunct values, that is to say, when moving upward, we find the highest place we can start from in order to arrive at both of the two conjunct values (we can also start and arrive at the same place, if we begin at our destination).

Conjunction >

(greatest lower bound, reading upwards)

1

       

        

b           

|

             n

                

        

0

 

Priest writes: “f is the meet on this lattice”. (On this wiki page, the greatest lower bound is called the “meet”.) For disjunction, we look for the least upper bound: when moving downward, we seek the lowest place we can start from to arrive at both values.

Disjunction ↓ <

(least upper bound, reading downwards)

1

       

        

b           

|

             n

                

        

0

 

Priest writes: f is the join. (On this wiki page, the least upper bound is called the “join”.) ]

As we saw in chapter 8, FDE can be formulated as a four-valued logic. V = {1, 0, b, n} – true (only), false (only), both and neither. D = {1, b}. The values are ordered as follows:

 

1

↗               ↖

b                                 n

↖                   ↗

0

 

f is the meet on this lattice; f is the join; f¬ maps 1 to 0, vice versa, and each of b and n to itself.

(245)

[contents]

 

 

 

 

 

 

11a.4.3

[KFDE, KL, and KK3]

 

[Our modal FDE logic is called KFDE. “If we ignore the value n in the non-modal case (that is, we insist that formulas take one of the values in {1, b, 0}) we get the logic LP. In the modal case, we get KLP. If we ignore the value b in the non-modal case, we get the logic K3. In the modal case, we get KK3” (245).]

 

[Recall from section 11a.2.8 that a many-valued modal logic is called KL. Here the L is a many-valued logic, and the K is a modal logic (see section 2.1 and section 2.3). The K part is structured in the following way:

An interpretation for this language is a triple ⟨W, R, v⟩. W is a non-empty set. Formally, W is an arbitrary set of objects. Intuitively, its members are possible worlds. R is a binary relation on W (so that, technically, R W×W). Thus, if u and v are in W, R may or may not relate them to each other. If it does, we will write uRv, and say that v is accessible from u. Intuitively, R is a relation of relative possibility, so that uRv means that, relative to u, situation v is possible. υ is a function that assigns a truth value (1 or 0) to each pair comprising a world, w, and a propositional parameter, p. We write this as vw(p) = 1 (or vw(p) = 0). Intuitively, this is read as ‘at world w, p is true (or false)’.

(p.21, section 2.3.3)

So that gives us the K in KL. The L is a many-valued logic, which has the structure:

a propositional many-valued logic is characterised by a structure ⟨V, D, {fc : c C}⟩, where V is the set of semantic values, D V is the set of designated values, and for each connective, c, fc is the truth function it denotes. An interpretation, v, assigns values in V to propositional parameters; the values of all formulas can | then be computed using the fcs; and a valid inference is one that preserves designated values in every interpretation.

(pp.242-243, section 11a.2.1; see section 7.2).

It would seem that for FDE, as a four-valued logic, its ⟨V, D, {fc : c C}⟩ would be filled out in the following way:

V = {1, 0, b, n}

D = {1, b}

C = {¬, ∧, ∨} (with A B as ¬A B)

fc; c C = {f¬, f, f}

 

f¬  
1 0
b b
n n
o 1

 

f 1 b n o
1 1 b n 0
b b b 0 0
n n 0 n 0
o 0 0 0 0

 

f 1 b n o
1 1 1 1 1
b 1 b 1 b
n 1 1 n n
o 1 b n 0

 

So when we combine this FDE four-valued semantics with modal semantics, our KL is more specifically KFDE. Now recall the exhaustion constraint from section 8.4.9 and 8.4.10. When applied to FDE, it disallows there being a neither value, giving us LP. Here we can also thereby obtain KLP. Or, if we apply the exclusion constraint (see section 8.4.6 and section 8.4.7), we can get K3, and thus here in our modal logics, KK3. (Note, the first K is for “Kripke” (our modal logic, see section 2.1.2) and the second one is for “Kleene” (which is  for our many-valued logics; see section 7.3.4)).]

KFDE is obtained by the general construction described. If we ignore the value n in the non-modal case (that is, we insist that formulas take one of the values in {1, b, 0}) we get the logic LP. In the modal case, we get KLP. If we ignore the value b in the non-modal case, we get the logic K3. In the modal case, we get KK3.

(245)

[contents]

 

 

 

 

 

 

11a.4.4

[The Relational Semantics of FDE]

 

[The equivalence between four-valued FDE truth-values and the four value-situations of the relational semantics are: v(A) = 1 iff Aρ1 and it is not the case that Aρ0 ; v(A) = b iff Aρ1 and Aρ0 ; v(A) = n iff it is not the case that Aρ1 and it is not the case that Aρ0 ; and v(A) = 0 iff it is not the case that Aρ1 and Aρ0 . The truth-falsity conditions for the connectives in the relational semantics are: A Bρ1 iff Aρ1 and Bρ1 ; A Bρ0 iff Aρ0 or Bρ0 ; A Bρ1 iff Aρ1 or Bρ1 ; A Bρ0 iff Aρ0 and Bρ0 ; ¬Aρ1 iff Aρ0 ; and ¬Aρ0 iff Aρ1 . “Validity is defined in terms of the preservation of relating to 1” (245).]

 

[Recall from section 8.2 that Priest originally formulates FDE using a relational semantics. Here he gives the equivalences between the four-values and the four value-situations along with the truth/falsity conditions for the connectives. Validity is preservation of 1.]

As we also saw in chapter 8, FDE can be formulated equivalently as a logic in which, instead of an evaluation function, v, there is a relation, ρ (not to be confused with the constraint on the accessibility relation), which relates a formula, A, to the values 1 (true) and 0 (false) as follows:

 

v(A) = 1 iff Aρ1 and it is not the case that Aρ0

v(A) = b iff Aρ1 and Aρ0

v(A) = n iff it is not the case that Aρ1 and it is not the case that Aρ0

v(A) = 0 iff it is not the case that Aρ1 and Aρ0

 

The appropriate truth/falsity conditions for the connectives are:

 

A Bρ1 iff Aρ1 and Bρ1

A Bρ0 iff Aρ0 or Bρ0

A Bρ1 iff Aρ1 or Bρ1

A Bρ0 iff Aρ0 and Bρ0

¬Aρ1 iff Aρ0

¬Aρ0 iff Aρ1

 

Validity is defined in terms of the preservation of relating to 1.

(245)

[contents]

 

 

 

 

 

 

11a.4.5

[The Relational Semantics of KFDE]

 

[KFDE has the same relational semantics but with world designations and with the following rules for the necessity and possibility operators: □Aρw1 iff for all w′ such that wRw′, Aρw1 ; □Aρw0 iff for some w′ such that wRw′, Aρw0 ; ◊Aρw1 iff for some w′ such that wRw′, Aρw1 ; ◊Aρw0 iff for all w′ such that wRw′, Aρw0 .]

 

[Priest next says that we can formulate KFDE firstly by using the above formulations from section 11a.4.4 by adding world designations, and secondly by formulating the truth/falsity conditions for the modal operators similarly. Recall from section 11a.2.6 that the modal operators for a many-valued modal logic would be given as:

vw(□A) = Glb{vw(A) : wRw′}

vw(◊A) = Lub{vw(A) : wRw′}

(p.242, section 11a.2.6 )

For necessity, we take the greatest lower bound. So in FDE, if a formula is related both to 1 and 0 in whatever accessible world, the greatest lower bound would be 0. These are the conditions for necessity in our modal version:

Aρw1 iff for all w′ such that wRw′, Aρw1

Aρw0 iff for some w′ such that wRw′, Aρw0

That would seem to fit the lower-bound articulation. Likewise for the possibility operator (see below). As such, I will try to list all the value equivalences and truth/falsity conditions for all the values and operators in KFDE formulated in the relational semantics.

 

vw(A) = 1 iff Aρw1 and it is not the case that Aρw0

vw(A) = b iff Aρw1 and Aρw0

vw(A) = n iff it is not the case that Aρw1 and it is not the case that Aρw0

vw(A) = 0 iff it is not the case that Aρw1 and Aρw0

 

A Bρw1 iff Aρw1 and Bρw1

A Bρw0 iff Aρ0 or Bρw0

 

A Bρw1 iff Aρw1 or Bρw1

A Bρw0 iff Aρw0 and Bρw0

 

¬Aρw1 iff Aρw0

¬Aρw0 iff Aρw1

 

Aρw1 iff for all w′ such that wRw′, Aρw1

Aρw0 iff for some w′ such that wRw′, Aρw0

 

Aρw1 iff for some w′ such that wRw′, Aρw1

Aρw0 iff for all w′ such that wRw′, Aρw0

(based on with quotation from p.245-246)

]

KFDE can be formulated in the same way. The facts of 11a.4.4 carry over with a subscript w to the vs and ρs. What of the truth/falsity conditions | of the modal operators if FDE is formulated in this way? They may be given, in a very natural way, as follows:

Aρw1 iff for all w′ such that wRw′, Aρw1

Aρw0 iff for some w′ such that wRw′, Aρw0

Aρw1 iff for some w′ such that wRw′, Aρw1

Aρw0 iff for all w′ such that wRw′, Aρw0

(246)

[contents]

 

 

 

 

 

 

11a.4.6

[The Rationale for the Modal Operator Truth/Falsity Conditions]

 

[Next Priest provides the argumentation for why the truth/falsity conditions are formulated the way they are.]

 

[(ditto)]

The argument for this is as follows. Consider vw(□A), that is Glb{vw(A) : wRw′}. This has four possible values.

1: In this case, for all w′ such that wRw′ the value of vw(A) is 1. So for all w′ such that wRw′, Aρw1 and it is not the case that Aρw0. In this case, the truth/falsity conditions give that □Aρw1 and it is not the case that □Aρw0, as required.

b: In this case, for all w′ such that wRw′, the value of vw(A) is 1 or b, and at least one is b. That is, for all w′ such that wRw′, Aρw1 and for at least one such w′, Aρw0. In this case, the truth/falsity conditions give that □Aρw1 and □Aρw0, as required.

n: In this case, for all w′ such that wRw′, the value of vw(A) is 1 or n, and at least one is n. That is, for all w′ such that wRw′, it is not the case that Aρw0 and for at least one such w′, it is not the case that Aρw1. In this case, the truth/falsity conditions give that it is not the case that □Aρw1 and it is not the case that □Aρw0, as required.

0: In this case, either there is some w′ such that wRw′ and vw(A) = 0, or there are w′ and w′′, such that wRw′, wRw′′, vw(A) = b and vw′′(A) = n. In the first case, for all w′ such that wRw′, Aρw′0 and it is not the case that Aρw1. In the second case, Aρw′′1 and Aρw′′0, and neither Aρw′′1 nor Aρw′′0. In either case, the truth/falsity conditions give that □Aρw0 and it is not the case that □Aρw1, as required.

The case for ◊ is similar, and is left as an exercise.

(264)

[contents]

 

 

 

 

 

 

11a.4.7

[Obtaining KLP]

 

[By adding a possible worlds exhaustion constraint to KFDE we can get KLP.]

 

[Recall the exhaustion constraint from section 8.4.9:

Exhaustion: for all p, either 1 or 0

i.e., every propositional parameter is either true or false – and maybe both. Then it is not difficult to check that, again, the same holds for every sentence, A. That is, nothing takes the value n.

(p.148, section 8.4.9)

In section 8.4.10 we saw that exhaustion-constrained FDE is equivalent to LP (see section 7.4). Priest seems to be saying that if in KFDE we add the world designations to the exhaustion constraint, we can get KLP. But I am not sure if that means it would be:

Exhaustion: for all p, either w1 or w0

or what else it would be.]

In the context of the relational semantics, LP is obtained by requiring that, for all p, either pρ1 or pρ0. (See 8.4.9.) The same is true with the appropriate subscript w on ρ for KLP.

(246)

[contents]

 

 

 

 

 

 

11a.4.8

[Obtaining KK3]

 

[By adding a possible worlds exclusion constraint to KFDE we can get KK3.]

 

[Now recall the exclusion constraint from section 8.4.6:

Exclusion: for no p, 1 and 0

| i.e., no propositional parameter is both true and false. Then it is not difficult to check that the same holds for every sentence, A. That is, nothing takes the value b.

(p.147-148, section 8.4.6)

In section 8.4.7 we saw that this gives us a logic equivalent to K3. So similarly to what we did above in section 11a.4.7, we can obtain KK3 by adding the possible worlds exclusion constraint to KFDE. So maybe it is formulated:

Exclusion: for no p, w1 and w0

But I have no idea how it should be written.]

In the context of the relational semantics, K3 is obtained by requiring that, for all p, not both pρ1 and pρ0. (See 8.4.6.) The same is true with the appropriate subscript w on ρ for KK3.

(246)

[contents]

 

 

 

 

 

 

 

11a.4.9

[Obtaining K]

 

[By adding both the exhaustion and exclusion constraints to KFDE, we get the classical modal logic K.]

 

[Next recall from section 8.4.12 that when we add both the exhaustion and exclusion constraints to FDE, we get something equivalent to classical logic. Thus by adding both the exhaustion and exclusion constraints to KFDE, we get the classical modal logic K.]

If we add both conditions in the non-modal case, we get classical logic. In the modal case, we get the classical modal logic K.

(247)

[contents]

 

 

 

 

 

 

11a.4.10

[Extensions of Our Many-Valued Modal Logics]

 

[We can apply the world accessibility relation constraints (like ρ, σ, τ, etc) to our specific many-valued modal logics to get such extensions as: KFDEρ, KLPρτ, KK3σ and so forth.]

 

[Next recall from section 3.2.3 the constraints on the accessibility relation that generate variations of a modal logic:

ρ (rho), reflexivity: for all w, wRw.

σ (sigma), symmetry: for all w1, w2, if w1Rw2, then w2Rw1.

τ (tau), transitivity: for all w1, w2, w3, if w1Rw2 and w2Rw3, then w1Rw3.

η (eta), extendability: for all w1, there is a w2 such that w1Rw2.

(p.36, section 3.2.3)

We saw in section 11a.2.8 that we can apply them to a many-valued modal logic KL to derive stronger logics, like KLρ, KLσ, KLρτ, and so forth. Thus we can apply them to our specific many-valued modal logics to get such extensions as: KFDEρ, KLPρτ, KK3σ and so forth.]

All the many-valued modal logics may be extended by adding the constraints on the accessibility relation ρ, σ and τ, to give KFDEρ, KLPρτ, KK3σ, etc.

(247)

[contents]

 

 

 

 

 

 

11a.4.11

[The Lack of Logical Truths in KFDE and KK3.]

 

[There are no logical truths (tautologies) in KFDE and KK3, because to be a logical truth means that the formula is true under all interpretations. But in KFDE and KK3, under any interpretation, every formula can be valued neither true nor false, and thus no formulas can be logical truths.]

 

[I may not grasp the next idea. Recall from section 1.3.4 that:

A is a logical truth (tautology) (⊨ A) iff it is a semantic consequence of the empty set of premises (φA), that is, every interpretation makes A true.

(p.5, section 1.3.4)

Now, in KFDE and KK3, there is always the option that a formula have neither value. That means that in these logics (and their extensions), they can never be logical truths, because that requires the formula to be true under all interpretations.]

Note that KFDE, KK3, and all their normal extensions have no logical truths. To see this, just consider the interpretation with one world, w, such that wRw, and for all p, neither pρw1 nor pρw0. An easy induction shows the same to be true for all formulas. (Details are left as an exercise.)

(247)

[contents]

 

 

 

 

 

 

11a.4.12

[The Monotonicity of These Logics]

 

[The interpretations for the logics of the family we are considering are monotonic.]

 

[Priest’s next point is that all of the interpretations for the logics here are monotonic. But this is not a concept I know about yet or could find explained elsewhere in this text, so I will need to come back to it later.]

Note also that interpretations for any logic in the family we are considering is monotonic, in the following sense. Let 12 iff the two interpretations have the same worlds and accessibility relation, and, in addition, for all propositional parameters, p, and all worlds, w:

if pρ1w1 then pρ2w1

if pρ1w0 then pρ2w0

where ρ1 and ρ2 are the evaluation relations of 1 and 2, respectively. If 12, the displayed conditions obtain for an arbitrary formula, A. The proof is by a simple induction, which is left as an exercise.

(247)

[contents]

 

 

 

 

 

 

 

11a.4.13

[Corollary]

 

[A corollary of this is “that ⊨K A iff ⊨KLPA (and similarly for Kρ and KLPρ, etc.)” (247).]

 

[Priest continues this discussion, but for the same reasons as above, I will need to come back to it later.]

A corollary is that ⊨K A iff ⊨KLPA (and similarly for Kρ and KLPρ, etc.). From right to left, the result is straightforward, since any interpretation of K is an interpretation of KLP. For the converse, suppose that ⊭KLP A. Then there is an interpretation, 2, such that A does not hold at some world, w0, in 2 (i.e., it is not the case that Aρw01). Let 1 be any classical interpretation obtained from 2 simply by resolving contradictory propositional parameters one way or the other. That is, when pρ2w1 and pρ2w0, only one of these holds for ρ1w. Then 12. By monotonicity, A does not hold at w0 in 1; and 1 is an interpretation for K.

(247)

[contents]

 

 

 

 

 

 

 

From:

 

Priest, Graham. 2008 [2001]. An Introduction to Non-Classical Logic: From If to Is, 2nd edn. Cambridge: Cambridge University.

 

 

 

 

 

 

No comments:

Post a Comment